From e4e21cdbbb6b85104788b3d3d337da3e2d9f3e4a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Oct 2003 19:36:34 +0000
Subject: Passage des notations de type dans type_scope

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

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 2c6addf3df..2e49fab040 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -45,10 +45,10 @@ Arguments Scope sig2 [type_scope type_scope type_scope].
 Arguments Scope sigS [type_scope type_scope].
 Arguments Scope sigS2 [type_scope type_scope type_scope].
 
-Notation "{ x : A  |  P }" := (sig A [x:A]P).
-Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q).
-Notation "{ x : A  &  P }" := (sigS A [x:A]P).
-Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q).
+Notation "{ x : A  |  P }" := (sig A [x:A]P) : type_scope.
+Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q) : type_scope.
+Notation "{ x : A  &  P }" := (sigS A [x:A]P) : type_scope.
+Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q) : type_scope.
 
 Add Printing Let sig.
 Add Printing Let sig2.
@@ -100,20 +100,24 @@ Inductive sumbool [A,B:Prop] : Set
     := left  : A -> {A}+{B}
      | right : B -> {A}+{B}
 
-where "{ A } + { B }" := (sumbool A B).
+where "{ A } + { B }" := (sumbool A B) : type_scope.
 
 Inductive sumor [A:Set;B:Prop] : Set
     := inleft  : A -> A+{B}
      | inright : B -> A+{B}
 
-where "A + { B }" := (sumor A B).
+where "A + { B }" := (sumor A B) : type_scope.
 
 (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
 
-Notation "B + { x : A | P }"     := B + (sig A [x:A]P) (only parsing).
-Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) (only parsing).
-Notation "B + { x : A & P }"     := B + (sigS A [x:A]P) (only parsing).
-Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) (only parsing).
+Notation "B + { x : A | P }"     := B + (sig A [x:A]P)
+  (only parsing) : type_scope.
+Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q)
+  (only parsing) : type_scope.
+Notation "B + { x : A & P }"     := B + (sigS A [x:A]P)
+  (only parsing) : type_scope.
+Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q)
+  (only parsing) : type_scope.
 
 (** Choice *)
 
-- 
cgit v1.2.3