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/Program/Combinators.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Program/Combinators.v')

diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 8813131d7b..18e55aefc6 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -40,8 +40,8 @@ Proof.
   reflexivity.
 Qed.
 
-Hint Rewrite @compose_id_left @compose_id_right : core.
-Hint Rewrite <- @compose_assoc : core.
+Global Hint Rewrite @compose_id_left @compose_id_right : core.
+Global Hint Rewrite <- @compose_assoc : core.
 
 (** [flip] is involutive. *)
 
-- 
cgit v1.2.3