From 826215450c44bb575e6ed2ab2ea8818131b996f4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 19 Jun 2012 11:36:27 +0000
Subject: BinInt: a forgotten scope for a notation

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

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 3a5eb8855e..f3f7b850ee 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1353,7 +1353,7 @@ Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope.
 Infix "÷" := Z.quot (at level 40, left associativity) : Z_scope.
 
 (* TODO : transition from Zdivide *)
-Notation "( x | y )" := (Z.divide x y) (at level 0).
+Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope.
 
 Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope.
 
-- 
cgit v1.2.3