From df076edfe673069decf9e8b0dc5f3b7941796060 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 5 Jul 2022 11:27:40 +0200
Subject: Add [#global] qualifier on Hint Rewrite (#439)

Adapt w.r.t. coq/coq#16004.
---
 common/Events.v | 4 ++++
 lib/Integers.v  | 8 ++++++++
 2 files changed, 12 insertions(+)

diff --git a/common/Events.v b/common/Events.v
index 0ada1207..2e076523 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -27,6 +27,9 @@ Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
 
+(** Backwards compatibility for Hint Rewrite locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 (** * Events and traces *)
 
 (** The observable behaviour of programs is stated in terms of
@@ -113,6 +116,7 @@ Proof.
   induction t1; intros; simpl. auto. decEq; auto.
 Qed.
 
+#[global]
 Hint Rewrite E0_left E0_right Eapp_assoc
              E0_left_inf Eappinf_assoc: trace_rewrite.
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 68bff3a0..10faeefa 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -20,6 +20,9 @@ Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits.
 Require Archi.
 
+(** Backwards compatibility for Hint Rewrite locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 (** * Comparisons *)
 
 Inductive comparison : Type :=
@@ -1168,6 +1171,7 @@ Proof.
   intros. unfold mone. rewrite testbit_repr; auto. apply Ztestbit_m1. lia.
 Qed.
 
+#[global]
 Hint Rewrite bits_zero bits_mone : ints.
 
 Ltac bit_solve :=
@@ -1244,6 +1248,7 @@ Proof.
   intros. unfold not. rewrite bits_xor; auto. rewrite bits_mone; auto.
 Qed.
 
+#[global]
 Hint Rewrite bits_and bits_or bits_xor bits_not: ints.
 
 Theorem and_commut: forall x y, and x y = and y x.
@@ -1652,6 +1657,7 @@ Proof.
   lia.
 Qed.
 
+#[global]
 Hint Rewrite bits_shl bits_shru bits_shr: ints.
 
 Theorem shl_zero: forall x, shl x zero = x.
@@ -1980,6 +1986,7 @@ Proof.
     lia. lia. lia. lia.
 Qed.
 
+#[global]
 Hint Rewrite bits_rol bits_ror: ints.
 
 Theorem shl_rolm:
@@ -2530,6 +2537,7 @@ Proof.
   rewrite testbit_repr; auto. apply Zsign_ext_spec. lia. 
 Qed.
 
+#[global]
 Hint Rewrite bits_zero_ext bits_sign_ext: ints.
 
 Theorem zero_ext_above:
-- 
cgit