1 files changed, 0 insertions, 17 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e7308f165..7143f8a34 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 *)
 (*******************************)