diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-29 20:31:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-29 20:31:57 +0000 |
| commit | d3defc5b6f4e804bd6d052d350a54176c169d914 (patch) | |
| tree | ff94ce4f1feae050b6dd6b160a709dd87d659a8f /theories/Bool/Bool.v | |
| parent | 5743ea67b5a615c419d349e891806828c0ddc549 (diff) | |
Ne pas mettre d'associatif a droite au niveau 3 en V7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4088 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/Bool.v')
| -rwxr-xr-x | theories/Bool/Bool.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 96160f091..d17741295 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -173,7 +173,8 @@ Definition negb := [b:bool]Cases b of end. Infix "||" orb (at level 4, left associativity) : bool_scope. -Infix "&&" andb (at level 3, left associativity) : bool_scope. +Infix "&&" andb (at level 3, no associativity) : bool_scope + V8only (at level 30, left associativity). Notation "!! b" := (negb b) (at level 0, right associativity) : bool_scope. Open Scope bool_scope. |