From 2f5383542e03484eff1bbcceb983d2cd0c721092 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 Oct 2003 10:45:17 +0000
Subject: Argument de except, error implicite seulement en v8; Changement 'as
 notation' en 'where notation'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Specif.v | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d17d3403eb..333a355001 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -96,13 +96,17 @@ End Projections.
 
 (** Extended_booleans *)
 
-Inductive sumbool [A,B:Prop] : Set as "{ A } + { B }"
+Inductive sumbool [A,B:Prop] : Set
     := left  : A -> {A}+{B}
-     | right : B -> {A}+{B}.
+     | right : B -> {A}+{B}
 
-Inductive sumor [A:Set;B:Prop] : Set as "A + { B }"
+where "{ A } + { B }" := (sumbool A B).
+
+Inductive sumor [A:Set;B:Prop] : Set
     := inleft  : A -> A+{B}
-     | inright : B -> A+{B}.
+     | inright : B -> A+{B}
+
+where "A + { B }" := (sumor A B).
 
 (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
 
@@ -168,6 +172,8 @@ Implicits except [1].
 V7only [
 Notation Except := (!except ?) (only parsing).
 Notation Error := (!error ?) (only parsing).
+V7only [Implicits error [].].
+V7only [Implicits except [].].
 ].
 Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
 Proof.
-- 
cgit v1.2.3