diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2003-01-24 12:28:37 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2003-01-24 12:28:37 +0000 |
commit | 6a0742a3aafd136a73d5014627d8c5751a788f9d (patch) | |
tree | aa68d6d3100cb024c1592d1e54ab908d66856dab /coq/example.v | |
parent | 631014bdaac8efaf7471f5be3c1a8204b1d47bcc (diff) |
Modifications for support of Coq-7.3.1+ and above (new module system).
Diffstat (limited to 'coq/example.v')
-rw-r--r-- | coq/example.v | 32 |
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. |