diff options
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 5f82cf5f26..8b1a1979fb 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -103,6 +103,8 @@ GEXTEND Gram TacArg(!@loc,MetaIdArg (!@loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> TacArg(!@loc,ConstrMayEval(ConstrTerm c)) + | IDENT "uconstr"; ":" ; c = Constr.constr -> + TacArg(!@loc,UConstr c) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> TacArg(!@loc, TacGeneric (genarg_of_ipattern ipat)) | r = reference; la = LIST0 tactic_arg -> |