diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2efe88c0c3..27f80fd75d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -446,9 +446,13 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) - | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l) - + IDENT "Transparent"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.transparent,l] + | IDENT "Opaque"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.Opaque, l] + | IDENT "Strategy"; l = + LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> + VernacSetOpacity l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid @@ -542,6 +546,13 @@ GEXTEND Gram [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l | -> [] ] ] ; + strategy_level: + [ [ IDENT "expand" -> Conv_oracle.Expand + | IDENT "opaque" -> Conv_oracle.Opaque + | n=INT -> Conv_oracle.Level (int_of_string n) + | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) + | IDENT "transparent" -> Conv_oracle.transparent ] ] + ; END GEXTEND Gram |