diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 56779d71f..4bb01a6a4 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -43,8 +43,10 @@ GEXTEND Gram ; constr: [ [ c = constr8 -> c -(* | IDENT "Context"; id = ident; IDENT "With"; c = constr8 -> + (*| IDENT "Context"; id = ident; IDENT "With"; c = constr8 -> <:ast< (CONTEXT $id $c) >>*) + | IDENT "Inst"; id = ident; "["; c = constr8; "]" -> + <:ast< (CONTEXT $id $c) >> | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 -> <:ast< (EVAL $c (REDEXP $rtc)) >> ] ] ; |