From 3ef5f35b0d7ec6f56f68e4319d6ec85bebaa19b8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 14:57:07 +0200
Subject: Parse specifically idents as destruction arguments.

This is for backward compatibility.
---
 src/g_ltac2.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

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
     ] ]
   ;
-- 
cgit v1.2.3