From ea4cd2f26f76194b0f02d0487dcfec36868dfa80 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 23 Oct 2002 09:26:07 +0000 Subject: Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3176 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zsyntax.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 77930d10de..ef9647413d 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -220,20 +220,20 @@ Syntax constr Module Z_scope. Delimiters "'Z:" Z_scope "'". -Infix NONA 4 "<=" Zle : Z_scope. -Infix NONA 4 "<" Zlt : Z_scope. -Infix NONA 4 ">=" Zge : Z_scope. -(*Infix NONA 4 ">" Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *) -Infix NONA 4 "?=" Zcompare : Z_scope. -Infix 3 "+" Zplus : Z_scope. -Infix 3 "-" Zminus : Z_scope. -Infix 2 "*" Zmult : Z_scope. +Infix 4 "+" Zplus : Z_scope. +Infix 4 "-" Zminus : Z_scope. +Infix 3 "*" Zmult : Z_scope. Distfix 0 "- _" Zopp : Z_scope. -Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 3) : Z_scope. -Notation NONA 4 "x <= y < z" (Zle x y)/\(Zlt y z) (y at level 3) : Z_scope. -Notation NONA 4 "x < y < z" (Zlt x y)/\(Zlt y z) (y at level 3) : Z_scope. -Notation NONA 4 "x < y <= z" (Zlt x y)/\(Zle y z) (y at level 3) : Z_scope. -Notation NONA 4 "x <> y" ~(eq Z x y) : Z_scope. +Infix NONA 5 "<=" Zle : Z_scope. +Infix NONA 5 "<" Zlt : Z_scope. +Infix NONA 5 ">=" Zge : Z_scope. +(*Infix NONA 5 ">" Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *) +Infix NONA 5 "?=" Zcompare : Z_scope. +Notation NONA 5 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 4) : Z_scope. +Notation NONA 5 "x <= y < z" (Zle x y)/\(Zlt y z) (y at level 4) : Z_scope. +Notation NONA 5 "x < y < z" (Zlt x y)/\(Zlt y z) (y at level 4) : Z_scope. +Notation NONA 5 "x < y <= z" (Zlt x y)/\(Zle y z) (y at level 4) : Z_scope. +Notation NONA 5 "x <> y" ~(eq Z x y) : Z_scope. (* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) Notation NONA 1 "|| x ||" (Zabs x) : Z_scope. -- cgit v1.2.3