diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/success/induct.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/success/induct.v')
-rw-r--r-- | test-suite/success/induct.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b8c6bf3f..1ed731f5 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. + |