From d4b3bb61d84cb2cd831a43b65dc55ef25fa8abaa Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 29 Jan 2003 18:56:05 +0000
Subject: Added a file for testing modules of coq (new version 7.4). Plus some
 modification to better backtrack modules.

---
 coq/example.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'coq/example.v')

diff --git a/coq/example.v b/coq/example.v
index 5d55a2ae..6f92e279 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -9,7 +9,7 @@
     $Id$
 *)
 
-Section sect.
+Module sect.
 
 Goal (A,B:Prop)(A /\ B) -> (B /\ A).
  Intros A B H.
@@ -32,5 +32,9 @@ End mod.
 
 Module Type newmod.
 Definition type1:=Set.
+
+Goal (n:nat)n=n.
+Auto.
+Save toto.
 End newmod.
 
-- 
cgit v1.2.3