diff options
author | 2001-08-30 08:07:57 +0000 | |
---|---|---|
committer | 2001-08-30 08:07:57 +0000 | |
commit | 08a35669ea650a408310154dc194bbbd400814a5 (patch) | |
tree | bfd8efadb4f7c0d78ff074f136b2da5fc0c34c9c /theories/Init/Specif.v | |
parent | 27b1061be797da05212500f16af9c88ac28849ee (diff) |
Fin de la modif Exc/option
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Specif.v')
-rwxr-xr-x | theories/Init/Specif.v | 17 |
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 *) (*******************************) |