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 ++++
 1 file changed, 4 insertions(+)

(limited to 'common')

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.
 
-- 
cgit