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/modules | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/ind.v | 34 | ||||
-rw-r--r-- | test-suite/modules/nested_mod_types.v | 26 |
2 files changed, 59 insertions, 1 deletions
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v index a4f9d3a2..3af94c3b 100644 --- a/test-suite/modules/ind.v +++ b/test-suite/modules/ind.v @@ -14,4 +14,36 @@ End M. Module N := M. -Check (N.f M.A).
\ No newline at end of file +Check (N.f M.A). + +(* Check use of equivalence on inductive types (bug #1242) *) + + Module Type ASIG. + Inductive t : Set := a | b : t. + Definition f := fun x => match x with a => true | b => false end. + End ASIG. + + Module Type BSIG. + Declare Module A : ASIG. + Definition f := fun x => match x with A.a => true | A.b => false end. + End BSIG. + + Module C (A : ASIG) (B : BSIG with Module A:=A). + + (* Check equivalence is considered in "case_info" *) + Lemma test : forall x, A.f x = B.f x. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + + (* Check equivalence is considered in pattern-matching *) + Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end. + + End C. + +(* Check subtyping of the context of parameters of the inductive types *) +(* Only the number of expected uniform parameters and the convertibility *) +(* of the inductive arities and constructors types are checked *) + +Module Type S. Inductive I (x:=0) (y:nat): Set := c: x=y -> I y. End S. +Module P : S. Inductive I (y':nat) (z:=y'): Set := c : 0=y' -> I y'. End P. diff --git a/test-suite/modules/nested_mod_types.v b/test-suite/modules/nested_mod_types.v new file mode 100644 index 00000000..f459f9ec --- /dev/null +++ b/test-suite/modules/nested_mod_types.v @@ -0,0 +1,26 @@ +Module Type T. + Module Type U. + Module Type V. + Variable b : nat. + End V. + Variable a : nat. + End U. + Declare Module u : U. + Declare Module v : u.V. +End T. + +Module F (t:T). +End F. + +Module M:T. + Module Type U. + Module Type V. + Variable b : nat. + End V. + Variable a : nat. + End U. + Declare Module u : U. + Declare Module v : u.V. +End M. + +Module FM := F M. |