diff options
| author | Arnaud Spiwack | 2014-07-29 13:19:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-29 17:16:29 +0200 |
| commit | 9e8316d8fd6a13966c21ef77d5fcba270bc9a32a (patch) | |
| tree | 99046866a67cf09557470d53e00aa9173fa87a7f | |
| parent | 52247f50fa9aed83cc4a9a714b6b8f779479fd9b (diff) | |
Untyped term in tactics: add an grammar entry to construct them.
The syntax is uconstr:term.
| -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 -> |