diff options
| -rw-r--r-- | ltac/g_ltac.ml4 | 3 |
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 ()) ] ] ; |