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".

1 files changed, 1 insertions, 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 ()) ] ]
   ;