summaryrefslogtreecommitdiff
path: root/test-suite/modules
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /test-suite/modules
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/ind.v34
-rw-r--r--test-suite/modules/nested_mod_types.v26
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.