1 files changed, 1 insertions, 0 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 3d873c7369..c1025ceba5 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -459,6 +459,7 @@ GEXTEND Gram
   ;
   destruction_arg:
     [ [ n = lnatural -> QElimOnAnonHyp n
+      | id = lident -> QElimOnIdent id
       | c = constr_with_bindings -> QElimOnConstr c
     ] ]
   ;