diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-28 19:36:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-28 19:36:34 +0000 |
| commit | e4e21cdbbb6b85104788b3d3d337da3e2d9f3e4a (patch) | |
| tree | 905d19a4b41abedf5f2f45dd5236f864e70ff786 /theories | |
| parent | bf7ba04c942f2b42f0ffa0c6f292ba638aec17fd (diff) | |
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
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Specif.v | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2c6addf3d..2e49fab04 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 *) |