Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

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.
+