From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001
From: coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 2 Aug 2002 17:17:42 +0000
Subject: Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/modules/modul.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test-suite/modules/modul.v

(limited to 'test-suite/modules/modul.v')

diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
new file mode 100644
index 000000000..ba333c525
--- /dev/null
+++ b/test-suite/modules/modul.v
@@ -0,0 +1,39 @@
+Mod M.
+  Parameter rel:nat -> nat -> Prop.
+
+  Axiom w : (n:nat)(rel O (S n)).
+
+  Hints Resolve w.
+
+  Grammar constr constr8 := 
+     not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+  
+  Print Hint *.
+
+  Lemma w1 : (O#(S O)).
+  Auto.
+  Save.
+
+EndM M.
+
+(*Lemma w1 : (M.rel O (S O)).
+Auto.
+*)
+
+Imp M.
+
+Print Hint *.
+Lemma w1 : (O#(S O)).
+Print Hint.
+Print Hint *.
+
+Auto.
+Save.
+
+Check (O#O).
+Locate rel.
+
+Locate M.
+
+Mod N:=Scratch.M.
+
-- 
cgit v1.2.3