From 45687f7f1ca127e881a80978f290b565ca629cf8 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sun, 5 Oct 2003 15:57:35 +0000
Subject: Rever to simplest example

---
 coq/example.v | 33 +--------------------------------
 1 file changed, 1 insertion(+), 32 deletions(-)

(limited to 'coq/example.v')

diff --git a/coq/example.v b/coq/example.v
index 5d076280..d9976ea7 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -1,45 +1,14 @@
 (*
     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.
-Recursive Tactic Definition  bar := Idtac.
  Elim H.
  Intros.
-  Lemma foo: (A:Set)Set.
-  Intro A.
-  Exact A.  
-  Save.
- Split.  
+ Split.
  Assumption.
  Assumption.
 Save and_comms.
-End sect.
-
-Section newmod.
-Definition type1:=Set.
-
-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].
-- 
cgit v1.2.3