Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 15 insertions, 19 deletions

diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 84942da1..9d24d6ce 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -1,39 +1,35 @@
 Module M.
-  Parameter rel:nat -> nat -> Prop.
+  Parameter rel : nat -> nat -> Prop.
 
-  Axiom w : (n:nat)(rel O (S n)).
+  Axiom w : forall n : nat, rel 0 (S n).
 
-  Hints Resolve w.
+  Hint Resolve w.
 
-  Grammar constr constr8 := 
-     not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+  (* <Warning> : Grammar is replaced by Notation *)
   
   Print Hint *.
 
-  Lemma w1 : (O#(S O)).
-  Auto.
-  Save.
+  Lemma w1 : rel 0 1.
+  auto.
+  Qed.
 
 End M.
 
+Locate Module M.
+
 (*Lemma w1 : (M.rel O (S O)).
 Auto.
 *)
 
 Import M.
 
-Print Hint *.
-Lemma w1 : (O#(S O)).
-Print Hint.
-Print Hint *.
-
-Auto.
-Save.
+Lemma w1 : rel 0 1.
+auto.
+Qed.
 
-Check (O#O).
+Check (rel 0 0).
 Locate rel.
 
-Locate Library M.
-
-Module N:=Top.M.
+Locate Module M.
 
+Module N := Top.M.