diff options
| author | herbelin | 2002-11-28 00:36:41 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-28 00:36:41 +0000 |
| commit | 7fb5fda36a3f758124a236e5387535c2471787ac (patch) | |
| tree | dd89a9f49b5d6a759f33d1d036110f22dfba1d92 | |
| parent | c379f867ca1f575744c843aaf816dab9cfe56a1a (diff) | |
Plus de précisions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 *) |