Fixing some problems with double induction.

Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.

Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".

Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).

See file induct.v for effect of changes.

4 files changed, 53 insertions, 45 deletions

diff --git a/CHANGES b/CHANGES
index a9fbfe29d0..cda16d3804 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,10 @@ Tactics
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
+- Serious bugs are fixed in tactic "double induction" (source of
+  incompatibilities as soon as the inductive types have dependencies in
+  the type of their constructors; "double induction" remains however
+  deprecated).
 
 Program
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 0954f3ddf2..99236e7707 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -145,8 +145,7 @@ let induction_trailer abs_i abs_j bargs =
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENLIST
-            [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids));
-	     simple_elimination (mkVar id)])
+            [revert ids; simple_elimination (mkVar id)])
           end }
           ))
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 750ec8fb1e..061c05b9b2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -239,52 +239,14 @@ let gl_make_case_nodep ind gl =
   (Sigma.to_evar_map sigma, r)
 
 let make_elim_branch_assumptions ba gl =
-  let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
-    match lb,lc with
-      | ([], _) ->
-          { ba = ba;
-            assums    = assums}
-      | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) ->
-	  makerec (recarg::indarg::assums,
-		   idrec::cargs,
-		   idrec::recargs,
-		   constargs,
-		   idind::indargs) tl idtl
-      | ((false::tl), ((id,_,_ as constarg)::idtl))      ->
-	  makerec (constarg::assums,
-		   id::cargs,
-		   id::constargs,
-		   recargs,
-		   indargs) tl idtl
-      | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions")
-  in
-  makerec ([],[],[],[],[]) ba.branchsign
-    (try List.firstn ba.nassums (pf_hyps gl)
-     with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions"))
+  let assums =
+    try List.rev (List.firstn ba.nassums (pf_hyps gl))
+    with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+  { ba = ba; assums = assums }
 
 let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
 
-let make_case_branch_assumptions ba gl =
-  let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 =
-    match p_0,p_1 with
-      | ([], _) ->
-          { ba = ba;
-            assums    = assums}
-      | ((true::tl), ((idrec,_,_ as recarg)::idtl)) ->
-	  makerec (recarg::assums,
-		   idrec::cargs,
-		   idrec::recargs,
-		   constargs) tl idtl
-      | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
-	  makerec (constarg::assums,
-		   id::cargs,
-		   recargs,
-		   id::constargs) tl idtl
-      | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions")
-  in
-  makerec ([],[],[],[]) ba.branchsign
-    (try List.firstn ba.nassums (pf_hyps gl)
-     with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions"))
+let make_case_branch_assumptions = make_elim_branch_assumptions
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 7ae60d9892..9413b8dae9 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -151,3 +151,46 @@ intros x H1 H.
 induction H.
 change (0 = z -> True) in IHrepr''.
 Abort.
+
+(* Test double induction *)
+
+(* This was failing in 8.5 and before because of a bug in the order of
+   hypotheses *)
+
+Inductive I2 : Type :=
+  C2 : forall x:nat, x=x -> I2.
+Goal forall a b:I2, a = b.
+double induction a b.
+Abort.
+
+(* This was leaving useless hypotheses in 8.5 and before because of
+   the same bug. This is a change of compatibility. *)
+
+Inductive I3 : Prop :=
+  C3 : forall x:nat, x=x -> I3.
+Goal forall a b:I3, a = b.
+double induction a b.
+Fail clear H. (* H should have been erased *)
+Abort.
+
+(* This one had quantification in reverse order in 8.5 and before *)
+(* This is a change of compatibility. *)
+
+Goal forall m n, le m n -> le n m -> n=m.
+intros m n. double induction 1 2.
+3:destruct 1. (* Should be "S m0 <= m0" *)
+Abort.
+
+(* Idem *)
+
+Goal forall m n p q, le m n -> le p q -> n+p=m+q.
+intros *. double induction 1 2.
+3:clear H2. (* H2 should have been erased *)
+Abort.
+
+(* This is unchanged *)
+
+Goal forall m n:nat, n=m.
+double induction m n.
+Abort.
+