From 08a35669ea650a408310154dc194bbbd400814a5 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 30 Aug 2001 08:07:57 +0000
Subject: Fin de la modif Exc/option

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Specif.v | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e7308f1651..7143f8a346 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -161,23 +161,6 @@ Definition error := None.
 Syntactic Definition Error := (error ?).
 Syntactic Definition Value := (value ?).
 
-(*
-Definition exc_rec :
- (A:Set; P:((Exc A)->Set))
- ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
- := option_rec.
-
-Definition exc_rect :
- (A:Set; P:((Exc A)->Type))
- ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
- := option_rect.
-
-Definition exc_ind :
- (A:Set; P:((Exc A)->Prop))
- ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
- := option_ind.
-*)
-
 (*******************************)
 (* Self realizing propositions *)
 (*******************************)
-- 
cgit v1.2.3