From 46ab3659dd1f2e4839064cfabc03bd19268fa44b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Mar 2018 14:47:06 +0200
Subject: Adapting standard library to the introduction of "Declare Scope".

Removing in passing two Local which are no-ops in practice.
---
 theories/Numbers/Integer/Abstract/ZDivEucl.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Numbers/Integer/Abstract')

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d7f25a6613..ab17bb6e1a 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -46,6 +46,7 @@ Module ZEuclidProp
 
  (** We put notations in a scope, to avoid warnings about
      redefinitions of notations *)
+ Declare Scope euclid.
  Infix "/" := D.div : euclid.
  Infix "mod" := D.modulo : euclid.
  Local Open Scope euclid.
-- 
cgit v1.2.3