diff options
Diffstat (limited to 'theories/Init/Notations.v')
| -rw-r--r-- | theories/Init/Notations.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 416647b4..3dc6385d 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v 8866 2006-05-28 16:21:04Z herbelin $ i*) +(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*) (** These are the notations whose level and associativity are imposed by Coq *) @@ -19,13 +19,13 @@ Reserved Notation "~ x" (at level 75, right associativity). (** Notations for equality and inequalities *) -Reserved Notation "x = y :> T" +Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x = y" (at level 70, no associativity). Reserved Notation "x = y = z" (at level 70, no associativity, y at next level). -Reserved Notation "x <> y :> T" +Reserved Notation "x <> y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x <> y" (at level 70, no associativity). @@ -49,6 +49,11 @@ Reserved Notation "- x" (at level 35, right associativity). Reserved Notation "/ x" (at level 35, right associativity). Reserved Notation "x ^ y" (at level 30, right associativity). +(** Notations for booleans *) + +Reserved Notation "x || y" (at level 50, left associativity). +Reserved Notation "x && y" (at level 40, left associativity). + (** Notations for pairs *) Reserved Notation "( x , y , .. , z )" (at level 0). |