From 4419a101a4f5a108be90cf4e420f0b6961e6caac Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Jan 2021 13:55:23 +0100
Subject: Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724
---
 theories/Structures/OrdersFacts.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Structures')

diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 4ac54d280a..c3e67b9d5a 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder').
  rewrite compare_gt_iff; intuition.
  Qed.
 
- Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+ Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
 
  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
  Proof.
-- 
cgit v1.2.3