Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
new file mode 100644
index 00000000..13c28418
--- /dev/null
+++ b/test-suite/modules/Tescik.v
@@ -0,0 +1,30 @@
+
+Module Type ELEM.
+  Parameter A:Set.
+  Parameter x:A.
+End ELEM.
+
+Module Nat.
+    Definition A:=nat.
+    Definition x:=O.
+End Nat. 
+
+Module List[X:ELEM].
+  Inductive list : Set := nil : list 
+		       | cons : X.A -> list -> list.
+ 
+  Definition head := 
+     [l:list]Cases l of 
+	  nil => X.x 
+	| (cons x _) => x
+     end.
+
+  Definition singl := [x:X.A] (cons x nil).
+  
+  Lemma head_singl : (x:X.A)(head (singl x))=x.
+  Auto.
+  Qed.
+
+End List.
+
+Module N:=(List Nat).