code cleaning + deals better with the new module system of Coq. Did

not test the fsfemacs. Will do before release.

1 files changed, 13 insertions, 8 deletions

diff --git a/coq/example.v b/coq/example.v
index 6f92e279..5d076280 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -9,7 +9,7 @@
     $Id$
 *)
 
-Module sect.
+Section sect.
 
 Goal (A,B:Prop)(A /\ B) -> (B /\ A).
  Intros A B H.
@@ -26,15 +26,20 @@ Recursive Tactic Definition  bar := Idtac.
 Save and_comms.
 End sect.
 
-Module mod.
+Section newmod.
 Definition type1:=Set.
-End mod.
 
-Module Type newmod.
-Definition type1:=Set.
-
-Goal (n:nat)n=n.
-Auto.
+Axiom A:False.
+Goal (n:nat)(S n)=n.
+Apply False_ind.
+Exact A.
 Save toto.
 End newmod.
 
+Extract Constant 
+
+Lemma Lem : (S O)=O.
+AutoRewrite [db].
+
+Hint Rewrite [toto] in db.
+AutoRewrite [db].