diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /test-suite/success/Case13.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'test-suite/success/Case13.v')
-rw-r--r-- | test-suite/success/Case13.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f19e24b8..f14725a8 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -67,3 +67,15 @@ Check (fun x => match x with | D _ => 1 end). +(* Check coercions against the type of the term to match *) +(* Used to fail in V8.1beta *) + +Inductive C : Set := c : C. +Inductive E : Set := e :> C -> E. +Check fun (x : E) => match x with c => e c end. + +(* Check coercions with uniform parameters (cf bug #1168) *) + +Inductive C' : bool -> Set := c' : C' true. +Inductive E' (b : bool) : Set := e' :> C' b -> E' b. +Check fun (x : E' true) => match x with c' => e' true c' end. |