Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 8d08f597..2f13b7c2 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -183,3 +183,33 @@ End HintCut.
 Goal forall (m : nat), exists n, m = n /\ m = n.
   intros m; eexists; split; [trivial | reflexivity].
 Qed.
+
+Section HintTransparent.
+
+  Definition fn (x : nat) := S x.
+
+  Create HintDb trans.
+
+  Hint Resolve eq_refl | (_ = _) : trans.
+
+  (* No reduction *)
+  Hint Variables Opaque : trans.  Hint Constants Opaque : trans.
+
+  Goal forall x : nat, fn x = S x.
+  Proof.
+    intros.
+    Fail typeclasses eauto with trans.
+    unfold fn.
+    typeclasses eauto with trans.
+  Qed.
+
+  (** Now allow unfolding fn *)
+  Hint Constants Transparent : trans.
+
+  Goal forall x : nat, fn x = S x.
+  Proof.
+    intros.
+    typeclasses eauto with trans.
+  Qed.
+
+End HintTransparent.