Imported Upstream version 8.0pl1upstream/8.0pl1

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 00000000..5612ea75
--- /dev/null
+++ b/test-suite/modules/modul.v
@@ -0,0 +1,39 @@
+Module 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.
+
+End M.
+
+(*Lemma w1 : (M.rel O (S O)).
+Auto.
+*)
+
+Import M.
+
+Print Hint *.
+Lemma w1 : (O#(S O)).
+Print Hint.
+Print Hint *.
+
+Auto.
+Save.
+
+Check (O#O).
+Locate rel.
+
+Locate M.
+
+Module N:=Top.M.
+