diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-03 13:32:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-03 13:32:50 +0200 |
| commit | c17b3248f3473ec464ab19196558533f621d796c (patch) | |
| tree | e3daa536a4db6f8fbd64a1c570f1f33a47302a3e /vernac/g_proofs.mlg | |
| parent | 4deb788a24b50eec3da66ed32bb85c185123c007 (diff) | |
| parent | bc5304a91cf4627063551422ad6e5a2cd1059897 (diff) | |
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
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 } ] ] |