From 7b207245cdfd7d91863441ef8e3fa4b99e830fac Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 Dec 2003 15:03:50 +0000
Subject: Duplication temporaire des règles de syntaxe des paires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories7/ZArith/Znumtheory.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories7/ZArith')

diff --git a/theories7/ZArith/Znumtheory.v b/theories7/ZArith/Znumtheory.v
index 4816395108..300ac520a0 100644
--- a/theories7/ZArith/Znumtheory.v
+++ b/theories7/ZArith/Znumtheory.v
@@ -33,7 +33,7 @@ Inductive Zdivide [a,b:Z] : Prop :=
 
 Notation "( a | b )" := (Zdivide a b) 
  (at level 0, a,b at level 10) : Z_scope
- V8only "a | b" (at level 260, no associativity).
+ V8only "( a | b )" (at level 0).
 
 (** Results concerning divisibility*)
 
-- 
cgit v1.2.3