From 05ae6109c6a233809ffa5ead5899a75d25f4cffd Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 16 Oct 2003 15:02:51 +0000 Subject: Suppression des surcharge de regles de grammaire en v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4650 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 3 +-- theories/ZArith/Zsyntax.v | 3 +-- theories/ZArith/fast_integer.v | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0e254c8e59..4fa0d7273a 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -175,8 +175,7 @@ Definition negb := [b:bool]Cases b of Infix "||" orb (at level 4, 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 - V8only. +Notation "- b" := (negb b) : bool_scope V8only Open Local Scope bool_scope. diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index d81dd968f8..d5055507b4 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -232,8 +232,7 @@ Module Z_scope. Infix LEFTA 4 "+" Zplus : Z_scope. Infix LEFTA 4 "-" Zminus : Z_scope. Infix LEFTA 3 "*" Zmult : Z_scope. -Notation "- x" := (Zopp x) (at level 0) : Z_scope - V8only (at level 40). +Notation "- x" := (Zopp x) : Z_scope V8only. Infix NONA 5 "<=" Zle : Z_scope. Infix NONA 5 "<" Zlt : Z_scope. Infix NONA 5 ">=" Zge : Z_scope. diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 180ab9fd2b..203d158309 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -64,7 +64,7 @@ with add_carry [x:positive]:positive -> positive := [y:positive] | xH xH => (xI xH) end. -V7only [Infix LEFTA 4 "+" add : positive_scope.]. +V7only [Notation "x + y" := (add x y) : positive_scope.]. V8Infix "+" add : positive_scope. Open Local Scope positive_scope. -- cgit v1.2.3