diff options
author | 2002-11-28 19:51:01 +0000 | |
---|---|---|
committer | 2002-11-28 19:51:01 +0000 | |
commit | e8fd8c89c43b2b1d00be631e888a1371cf05d0c0 (patch) | |
tree | b423dddfb48bce70f2959ff9ebf140127efdda0b | |
parent | 6aedc1b6c4047a206e2e02aea77cab23afa534a6 (diff) |
Simplification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Init/SpecifSyntax.v | 27 |
1 files changed, 10 insertions, 17 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 1fd9d9930..c3934e7b8 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -14,11 +14,9 @@ Require Specif. (** Symbolic notations for things in [Specif.v] *) (* At level 1 to factor with {x:A|P} etc *) -Notation "{ A } + { B }" := (sumbool A B) - (at level 1, A at level 10, B at level 10). +Notation "{ A } + { B }" := (sumbool A B) (at level 1). -Notation "A + { B }" := (sumor A B) - (at level 4, B at level 10, left associativity). +Notation "A + { B }" := (sumor A B) (at level 4, left associativity). Notation ProjS1 := (projS1 ? ?). Notation ProjS2 := (projS2 ? ?). @@ -26,31 +24,26 @@ Notation Except := (except ?). Notation Error := (error ?). Notation Value := (value ?). -Notation "{ x : A | P }" := (sig A [x:A]P) - (at level 1, x at level 10). +Notation "{ x : A | P }" := (sig A [x:A]P) (at level 1). +Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) (at level 1). -Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) - (at level 1, x at level 10). +Notation "{ x : A & P }" := (sigS A [x:A]P) (at level 1). +Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1). -Notation "{ x : A & P }" := (sigS A [x:A]P) - (at level 1, x at level 10). - -Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) - (at level 1, x at level 10). (** Extra factorization of parsing rules *) (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) Notation "B + { x : A | P }" := B + ({x:A | P}) - (at level 4, x at level 10, left associativity, only parsing). + (at level 4, left associativity, only parsing). Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q}) - (at level 4, x at level 10, left associativity, only parsing). + (at level 4, left associativity, only parsing). Notation "B + { x : A & P }" := B + ({x:A & P}) - (at level 4, x at level 10, left associativity, only parsing). + (at level 4, left associativity, only parsing). Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q}) - (at level 4, x at level 10, left associativity, only parsing). + (at level 4, left associativity, only parsing). |