diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/induct.v | 44 |
1 files changed, 0 insertions, 44 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4983ee3c0d..615350c58c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -154,50 +154,6 @@ 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 *) - -Set Warnings "-deprecated". - -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. - (* Mentioned as part of bug #12944 *) Inductive test : Set := cons : forall (IHv : nat) (v : test), test. |