diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-03-30 16:28:21 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-07-02 16:27:18 +0200 |
commit | 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 (patch) | |
tree | fb2951e3aee66c93f66c2bced46759a99baf3f46 /test-suite/success | |
parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) |
hints: add Hint Variables/Constants Opaque/Transparent commands
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Hints.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 717dc0deb..ebf5b094e 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. |