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 /vernac/g_proofs.mlg | |
| 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 'vernac/g_proofs.mlg')
| -rw-r--r-- | vernac/g_proofs.mlg | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 72db53f68..cccdbfc91 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -117,8 +117,12 @@ GRAMMAR EXTEND Gram | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> { HintsResolveIFF (false, lc, n) } | IDENT "Immediate"; lc = LIST1 reference_or_constr -> { HintsImmediate lc } - | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (lc, true) } - | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (lc, false) } + | IDENT "Variables"; IDENT "Transparent" -> { HintsTransparency (HintsVariables, true) } + | IDENT "Variables"; IDENT "Opaque" -> { HintsTransparency (HintsVariables, false) } + | IDENT "Constants"; IDENT "Transparent" -> { HintsTransparency (HintsConstants, true) } + | IDENT "Constants"; IDENT "Opaque" -> { HintsTransparency (HintsConstants, false) } + | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, true) } + | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, false) } | IDENT "Mode"; l = global; m = mode -> { HintsMode (l, m) } | IDENT "Unfold"; lqid = LIST1 global -> { HintsUnfold lqid } | IDENT "Constructors"; lc = LIST1 global -> { HintsConstructors lc } ] ] |