diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ca5f582d9f..c93acba58b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -56,9 +56,10 @@ GEXTEND Gram constr: [ [ c = constr8 -> c | IDENT "Inst"; id = ident; "["; c = constr8; "]" -> - <:ast< (CONTEXT $id $c) >> + <:ast<(CONTEXT $id $c)>> | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 -> - <:ast< (EVAL $c (REDEXP $rtc)) >> ] ] + <:ast<(EVAL $c (REDEXP $rtc))>> + | IDENT "Check"; c = constr8 -> <:ast<(CHECK $c)>> ] ] ; lconstr: [ [ c = constr10 -> c ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 2beb62f243..ec482d43d0 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -145,6 +145,7 @@ GEXTEND Gram <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >> | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> + | IDENT "Check"; c = Constr.constr -> <:ast<(COMMAND (CHECK $c))>> | st = simple_tactic -> st | id = lqualid; la = LIST1 tactic_atom0 -> <:ast< (APP $id ($LIST $la)) >> @@ -164,6 +165,7 @@ GEXTEND Gram <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >> | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> + | IDENT "Check"; c = Constr.constr -> <:ast<(COMMAND (CHECK $c))>> | "'"; c = constrarg -> c ] ] ; lqualid: |