From 6fbaac4bea11324e6c6785e8a5a7e4334ebcea1e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 17:22:26 +0200
Subject: Allow [uconstr:c] as argument of a tactic.

---
 parsing/g_ltac.ml4 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 4be4aa4ae7..d6f45d9f49 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -127,6 +127,7 @@ GEXTEND Gram
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
       | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
+      | IDENT "uconstr"; ":" ; c = Constr.constr -> UConstr c
       | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
         TacGeneric (genarg_of_ipattern ipat)
       | a = may_eval_arg -> a
-- 
cgit v1.2.3