Compatibility with 8.4 in the heuristic used to build the induction

hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.

2 files changed, 31 insertions, 4 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 599d42ee49..d1ab3cb38e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2742,7 +2742,7 @@ 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 args =
+  let rec atomize_one i params args =
     if Int.equal i nparams then
       let t = applist (hd, params @ List.map mkVar args) in
       Proofview.V82.tactic
@@ -2753,7 +2753,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 	| Var id when not (List.mem id args) &&
                       not (List.exists (occur_var env id) params) ->
             (* We know that the name can be cleared after destruction *)
-	    atomize_one (i-1) (id::args)
+	    atomize_one (i-1) params (id::args)
 	| _ ->
             let id = match kind_of_term c with
             | Var id -> id
@@ -2763,9 +2763,9 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
             let x = fresh_id_in_env args id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
-	      (atomize_one (i-1) (x::args))
+	      (atomize_one (i-1) (List.map (replace_term c (mkVar x)) params) (x::args))
   in
-  atomize_one (List.length argl) []
+  atomize_one (List.length argl) params []
   end
 
 let find_atomic_param_of_ind nparams indtyp =
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4b0b5d01c1..0d0466cb58 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -113,3 +113,30 @@ induction x as [|n IHn].
 2:change (n = 0) in IHn. (* We don't want a generalization over cond *)
 Abort.
 End S3.
+
+(* These examples show somehow arbitrary choices of generalization wrt
+   to indices, when those indices are not linear. We check here 8.4
+   compatibility: when an index is a subterm of a parameter of the
+   inductive type, it is not generalized. *)
+
+Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z.
+
+Goal forall x, 0 = x -> repr x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Goal forall x, 0 = S x -> repr (S x) (S x) -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z.
+
+Goal forall x, 0 = x -> repr' x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr'.
+Abort.