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 /CHANGES | |
| 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 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -52,6 +52,9 @@ Vernacular Commands - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. +- New Set Hint Variables/Constants Opaque/Transparent commands for setting + globally the opacity flag of variables and constants in hint databases, + overwritting the opacity set of the hint database. Coq binaries and process model |