diff --git a/CHANGELOG.md b/CHANGELOG.md index 3073851fd2fa142c69600e6f370bdbb1b11ae47d..e1c0d208dca169302d879fa8576eb9212761ce00 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,7 +38,7 @@ lemma. **Changes in `bi`:** -* Add hints for `match _ with _ end` (and thus `if _ then _ else` and +* Add instances for `match _ with _ end` (and thus `if _ then _ else` and `'(_, _)` pair destructuring) for `Persistent`, `Affine`, `Absorbing`, `Timeless`, and `Plain`. (by Sanjit Bhat) diff --git a/tests/bi.v b/tests/bi.v index d13b3ec59e04a71352bf242a198fc419c34253da..d95b30730375f1836455bf68889b505e3e2ef94a 100644 --- a/tests/bi.v +++ b/tests/bi.v @@ -102,7 +102,7 @@ Section internal_eq_ne. Proof. solve_proper. Qed. End internal_eq_ne. -Section tc_match. +Section instances_for_match. Context {PROP : bi}. Lemma match_persistent : @@ -132,9 +132,9 @@ Section tc_match. Proof. apply _. Qed. Check "match_def_unfold_fail". - (* Don't want hint to unfold def's. *) + (* Don't want instances to unfold def's. *) Definition match_foo (b : bool) : PROP := if b then False%I else False%I. Lemma match_def_unfold_fail b : Persistent (match_foo b). Proof. Fail apply _. Abort. -End tc_match. +End instances_for_match.