From 6a0742a3aafd136a73d5014627d8c5751a788f9d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Fri, 24 Jan 2003 12:28:37 +0000
Subject: Modifications for support of Coq-7.3.1+ and above (new module
 system).

---
 coq/example.v | 32 +++++++++++++++++++++++++++-----
 1 file changed, 27 insertions(+), 5 deletions(-)

(limited to 'coq/example.v')

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.
 
-- 
cgit v1.2.3