From 593e7cf7a08d1549c7e0e6b0a55931bb3aaefa5c Mon Sep 17 00:00:00 2001
From: Sanjit Bhat <sanjit.bhat@gmail.com>
Date: Fri, 16 Aug 2024 13:36:10 -0400
Subject: [PATCH] hints -> instances
---
CHANGELOG.md | 2 +-
tests/bi.v | 6 +++---
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3073851fd..e1c0d208d 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 d13b3ec59..d95b30730 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.
--
GitLab