diff options
| -rw-r--r-- | theories/Init/LogicSyntax.v | 2 | ||||
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 3a08dd529f..fda1cde030 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -14,8 +14,8 @@ Require Export Logic. Notation "< P , Q > { p , q }" := (conj P Q p q) (at level 1). -Notation "x = y" := (eq ? x y) (at level 5, no associativity). Notation "~ x" := (not x) (at level 5, right associativity). +Notation "x = y" := (eq ? x y) (at level 5, no associativity). Infix RIGHTA 6 "/\\" and. Infix RIGHTA 7 "\\/" or. diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 6593ca8bbd..0264df84b7 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -12,8 +12,8 @@ Require Logic_Type. (** Symbolic notations for things in [Logic_type.v] *) -Notation "x == y" := (eqT ? x y) (at level 5). -Notation "x === y" := (identityT ? x y) (at level 5). +Notation "x == y" := (eqT ? x y) (at level 5, no associativity). +Notation "x === y" := (identityT ? x y) (at level 5, no associativity). (* Order is important to give printing priority to fully typed ALL and EX *) |