From 9daf902b767c7ea44db606f62e21142d2910f8c1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 25 Nov 2005 12:21:39 +0000
Subject: Added Module/End

---
 coq/example.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'coq/example.v')

diff --git a/coq/example.v b/coq/example.v
index 95a9adac..f482f2ab 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -4,6 +4,8 @@
     $Id$
 *)
 
+Module Example.
+
 Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
   intros A B.
   intros H.
@@ -12,3 +14,8 @@ Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
   assumption.
   assumption.
 Save and_comms.
+
+End Example.
+
+
+
-- 
cgit v1.2.3