diff options
author | 2002-01-31 13:07:40 +0000 | |
---|---|---|
committer | 2002-01-31 13:07:40 +0000 | |
commit | d3ca56683d0977ed4cb7acc0d61c5d83ecc939c1 (patch) | |
tree | afb628657007ff33cdc2db21e769da76fe6c3d19 /theories/Init | |
parent | 4fef76aefe06938fc724e66c08ff51b501cf0dfa (diff) |
changement generation de schema d'elimination, False_rec est primitif, Constructor tac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
-rwxr-xr-x | theories/Init/Specif.v | 42 |
1 files changed, 0 insertions, 42 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 389b532f3..2ec58c560 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -161,37 +161,6 @@ Definition error := None. Syntactic Definition Error := (error ?). Syntactic Definition Value := (value ?). -(*******************************) -(* Self realizing propositions *) -(*******************************) - -(* [False -> C] can be proved for [C:Set] using informative - elimination for equality - - [Axiom False_rec : (P:Set)False->P.] - -*) - -Definition Q:=[P:Set][b:bool]if b then unit else P. - -Lemma False_rec : (P:Set)False->P. -Intros. -Change (Q P false). -Cut true=false. -Intro H1; Case H1. -Exact tt. -Contradiction. -Save. - -Lemma False_rect: (C:Type)False->C. -Proof. - Intros. - Cut Empty_set. - NewDestruct 1. - Elim H. -Qed. - - Definition except := False_rec. (* for compatibility with previous versions *) Syntactic Definition Except := (except ?). @@ -203,17 +172,6 @@ Proof. Apply (h2 h1). Qed. -(*i is now generated -Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C. -Proof. - Intros A B C F AB; Apply F; Elim AB; Auto. -Qed. -i*) - -(*i is now a theorem -Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b). -i*) - Hints Resolve left right inleft inright : core v62. (*********************************) |