From 9e8316d8fd6a13966c21ef77d5fcba270bc9a32a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 13:19:29 +0200
Subject: Untyped term in tactics: add an grammar entry to construct them.

The syntax is uconstr:term.
---
 parsing/g_ltac.ml4 | 2 ++
 1 file changed, 2 insertions(+)

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 ->
-- 
cgit v1.2.3