blob: 5d07628053d8cee2b3298ab25b64dc815026e64e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
(*
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.
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].
|
