Preserving the good effect of 014e5ac92a on not leaving dangling local

definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).

3 files changed, 38 insertions, 9 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ab0cd6fb3c..34fd8a8beb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2743,35 +2743,52 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   let hd,argl = decompose_app indtyp in
   let params = List.firstn nparams argl in
   (* le gl est important pour ne pas préévaluer *)
-  let rec atomize_one i params args =
+  let rec atomize_one i args avoid =
     if Int.equal i nparams then
-      let t = applist (hd, params @ List.map mkVar args) in
+      let t = applist (hd, params@args) in
       Proofview.V82.tactic
         (change_in_hyp None (fun _ sigma -> sigma, t) (hyp0,InHypTypeOnly))
     else
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-	| Var id when not (List.mem id args) &&
+	| Var id when not (List.exists (occur_var env id) args) &&
                       not (List.exists (occur_var env id) params) ->
-            (* We know that the name can be cleared after destruction *)
-	    atomize_one (i-1) params (id::args)
+            (* Based on the knowledge given by the user, all
+               constraints on the variable are generalizable in the
+               current environment so that it is clearable after destruction *)
+	    atomize_one (i-1) (c::args) (id::avoid)
 	| _ ->
+            if List.exists (dependent c) params ||
+               List.exists (dependent c) args
+            then
+              (* This is a case where the argument is constrained in a
+                 way which would require some kind of inversion; we
+                 follow the (old) discipline of not generalizing over
+                 this term, since we don't try to invert the
+                 constraint anyway. *)
+	      atomize_one (i-1) (c::args) avoid
+            else
+            (* We reason blindly on the term and do as if it were
+               generalizable, ignoring the constraints coming from
+               its structure *)
             let id = match kind_of_term c with
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_type_of gl in
             id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
-            let x = fresh_id_in_env args id env in
+            let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
-	      (atomize_one (i-1) (List.map (replace_term c (mkVar x)) params) (x::args))
+	      (atomize_one (i-1) (mkVar x::args) (x::avoid))
   in
-  atomize_one (List.length argl) params []
+  atomize_one (List.length argl) [] []
   end
 
 let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
-  List.map destVar (snd (List.chop nparams argl))
+  let params,args = List.chop nparams argl in
+  let test c = isVar c && not (List.exists (dependent c) params) in
+  List.map destVar (List.filter test args)
 
 (* [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 2aa07cde1b..56cdf18e68 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -396,6 +396,7 @@ 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 *)
+Abort.
 
 (* Check clearing of names *)
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 0d0466cb58..3715f65f6c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -140,3 +140,14 @@ intros x H1 H.
 induction H.
 change True in IHrepr'.
 Abort.
+
+(* In this case, generalization was done in 8.4 and we preserve it; this
+   is arbitrary choice  *)
+
+Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z.
+
+Goal forall x, 0 = x -> repr'' x x -> True.
+intros x H1 H.
+induction H.
+change (0 = z -> True) in IHrepr''.
+Abort.