Modifications for support of Coq-7.3.1+ and above (new module system).

1 files changed, 27 insertions, 5 deletions

diff --git a/coq/example.v b/coq/example.v
index 5a3c5b59..5d55a2ae 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -1,14 +1,36 @@
 (*
     Example proof script for Coq Proof General.
+
+    This is a legal script for coq 7.x, with
+    imbricated proofs definitions.
+
+    Replace Section by Module (>= coq-7.4).
  
     $Id$
 *)
 
+Section sect.
+
 Goal (A,B:Prop)(A /\ B) -> (B /\ A).
-  Intros A B H.
-  Induction H.
-  Apply conj.
-  Assumption.
-  Assumption.
+ Intros A B H.
+Recursive Tactic Definition  bar := Idtac.
+ Elim H.
+ Intros.
+  Lemma foo: (A:Set)Set.
+  Intro A.
+  Exact A.  
+  Save.
+ Split.  
+ Assumption.
+ Assumption.
 Save and_comms.
+End sect.
+
+Module mod.
+Definition type1:=Set.
+End mod.
+
+Module Type newmod.
+Definition type1:=Set.
+End newmod.