diff options
author | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /test-suite/success | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Cases.v | 6 | ||||
-rw-r--r-- | test-suite/success/set.v | 15 |
2 files changed, 19 insertions, 2 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index f445ca8e..c9a3c08e 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1865,3 +1865,9 @@ Type (fun n => match n with | Z0 => true | _ => false end). + +(* Check that types with unknown sort, as A below, are not fatal to + the pattern-matching compilation *) + +Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := + match p with eq_refl => u end. diff --git a/test-suite/success/set.v b/test-suite/success/set.v index 23019275..8116e897 100644 --- a/test-suite/success/set.v +++ b/test-suite/success/set.v @@ -1,8 +1,19 @@ +(* This used to fail in 8.0pl1 *) + Goal forall n, n+n=0->0=n+n. intros. - -(* This used to fail in 8.0pl1 *) set n in * |-. +Abort. + +(* This works from 8.4pl1, since merging of different instances of the + same metavariable in a pattern is done modulo conversion *) + +Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). + +Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H. +intros. +set (f _ _). +Abort. |