Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"

This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6.

1 files changed, 2 insertions, 1 deletions

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