From e01dabf9f7aa530c4c70aadf464097cd102b1df6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 10:19:44 +0200
Subject: Fixing parsing of constr argument of ltac functions at level 8 in the
 presence of entries starting with a non-terminal such as "b ^2".

---
 ltac/g_ltac.ml4 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index df499a2c9c..a3895e3401 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -175,8 +175,7 @@ GEXTEND Gram
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
     [ [ a = tactic_arg -> a
-      | r = reference -> Reference r
-      | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
+      | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
       (* Unambigous entries: tolerated w/o "ltac:" modifier *)
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
-- 
cgit v1.2.3