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/Structures/OrdersFacts.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Structures')

diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 87df6b479d..60c64d306b 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType').
   Module OrderTac := OT_to_OrderTac O.
   Ltac order := OrderTac.order.
 
+  Declare Scope order.
   Notation "x <= y" := (~lt y x) : order.
   Infix "?=" := compare (at level 70, no associativity) : order.
 
-- 
cgit v1.2.3