diff options
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 } ] ] |