Argument implicite pour None, error, except

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4620 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 10 insertions, 3 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 33eb6a322..d216ac2e7 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 7a05a89f7..d17d3403e 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.