From 4249ab5cac5bb0d638400b14c389ded98b3c8ea8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Oct 2014 08:44:12 +0100
Subject: Making destruct on idents with maximal implicit arguments working, by
 keeping them as open holes. When these arguments are class instances, this
 restores compatibility with the 8.4 search for subterms from non-fully
 applied patterns which was using conversion on the instances.

---
 tactics/tacinterp.ml          |  2 +-
 test-suite/success/destruct.v | 25 +++++++++++++++++++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cc09170107..7f18065fe6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -958,7 +958,7 @@ let interp_induction_arg ist gl arg =
 	else
           let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
           let f env sigma = 
-            let (sigma,c) = interp_constr ist env sigma c in
+            let (sigma,c) = interp_open_constr ist env sigma c in
             sigma,(c,NoBindings) in
           keep,ElimOnConstr f
 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 4704a08e59..c6eff3eebe 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -252,3 +252,28 @@ destruct H.
 - exact I.
 - reflexivity.
 Qed.
+
+(* Check destruct on idents with maximal implicit arguments - which did
+   not work in 8.4 *)
+
+Parameter f : forall {n:nat}, n=n -> nat.
+Goal f (eq_refl 0) = 0.
+destruct f.
+Abort.
+
+(* This one was working in 8.4 (because of full conv on closed arguments) *)
+
+Class A.
+Instance a:A.
+Goal forall f : A -> nat -> nat, f (id a) 0 = f a 0.
+intros.
+destruct (f _).
+change (0=0).
+Abort.
+
+(* This one was not working in 8.4 because an occurrence of f was
+   remaining, blocking the "clear f" *)
+
+Goal forall f : A -> nat -> nat, f a 0 = f a 1.
+intros.
+destruct f.
-- 
cgit v1.2.3