diff options
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 | ||||
| -rwxr-xr-x | theories/Init/Specif.v | 11 |
2 files changed, 10 insertions, 3 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 33eb6a3221..d216ac2e75 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -50,6 +50,8 @@ Hints Resolve refl_identity : core v62. Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). +Implicits None [1]. + (** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) Inductive sum [A,B:Set] : Set diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 7a05a89f75..d17d3403eb 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -157,13 +157,18 @@ End Choice_lemmas. Definition Exc := option. Definition value := Some. -Definition error := None. +Definition error := !None. + +Implicits error [1]. Definition except := False_rec. (* for compatibility with previous versions *) -Notation Except := (except ?). -Notation Error := (error ?). +Implicits except [1]. +V7only [ +Notation Except := (!except ?) (only parsing). +Notation Error := (!error ?) (only parsing). +]. Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C. Proof. Intros A C h1 h2. |