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/Numbers/Integer/Abstract/ZAdd.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Integer/Abstract/ZAdd.v')

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 0c097b6773..9d9244eefb 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -18,7 +18,7 @@ Include ZBaseProp Z.
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
 
-Hint Rewrite opp_0 : nz.
+Global Hint Rewrite opp_0 : nz.
 
 Theorem add_pred_l n m : P n + m == P (n + m).
 Proof.
-- 
cgit v1.2.3