1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index b8c6bf3ff..1ed731f50 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.
+