From 014e5ac92a2338f8820be63618c5b0dd631744de Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Nov 2014 09:33:16 +0100
Subject: Removing yet another source of remaining local definitions.

---
 tactics/tactics.ml            | 13 +------------
 test-suite/success/destruct.v |  4 ++++
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6603c82cd2..ab0cd6fb3c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2771,18 +2771,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 
 let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
-  let argv = Array.of_list argl in
-  let params = List.firstn nparams argl in
-  let indvars = ref Id.Set.empty in
-  for i = nparams to (Array.length argv)-1 do
-    match kind_of_term argv.(i) with
-      | Var id
-          when not (List.exists (occur_var (Global.env()) id) params) ->
-	  indvars := Id.Set.add id !indvars
-      | _ -> ()
-  done;
-  Id.Set.elements !indvars;
-
+  List.map destVar (snd (List.chop nparams argl))
 
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
    ind. var.) and [aftertoclear] (coming after the ind. var.)  of hyps
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index f5848ffe0e..2aa07cde1b 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -393,6 +393,10 @@ intros * Heq H Heq'.
 destruct H.
 Abort.
 
+Goal 2=1 -> 1=0.
+intro H. destruct H.
+Fail (match goal with n:nat |- _ => unfold n end). (* Check that no let-in remains *)
+
 (* Check clearing of names *)
 
 Inductive eqnat (x : nat) : nat -> Prop :=
-- 
cgit v1.2.3