diff options
Diffstat (limited to 'user-contrib/Ltac2/g_ltac2.mlg')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 65b61a0d93..548e12d611 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -213,7 +213,7 @@ GRAMMAR EXTEND Gram | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c } | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c } | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c } - | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } + | IDENT "pat"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c } | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid } | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } |