diff options
| author | Matthieu Sozeau | 2017-03-30 16:28:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-07-02 16:27:18 +0200 |
| commit | 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 (patch) | |
| tree | fb2951e3aee66c93f66c2bced46759a99baf3f46 /theories | |
| 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 'theories')
| -rw-r--r-- | theories/Init/Logic.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 10ca9ecc92..817581cb20 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -29,6 +29,13 @@ Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. +(** Create the "core" hint database, and set its transparent state for + variables and constants explicitely. *) + +Create HintDb core. +Hint Variables Opaque : core. +Hint Constants Opaque : core. + Hint Unfold not: core. (** [and A B], written [A /\ B], is the conjunction of [A] and [B] |