From f1a0e13b3b1dde9492e54c04e8dfc3ccd07ee6c2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 11:39:26 +0000
Subject: Argument implicite pour None, error, except

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4620 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v |  2 ++
 theories/Init/Specif.v    | 11 ++++++++---
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'theories/Init')

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.
-- 
cgit v1.2.3