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

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.
 
 (*********************************)