Adapt w.r.t. coq/coq#16004. (#606)

PrincetonUniversity · Jul 19, 2022 · 0e364d0 · 0e364d0
1 parent 349165e
commit 0e364d0
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 0 deletions.
diff --git a/compcert/common/Events.v b/compcert/common/Events.v
@@ -27,6 +27,9 @@ Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
 
+(** Ignore Hint Rewrite global attribute for Coq 8.13 *)
+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/compcert/lib/Integers.v b/compcert/lib/Integers.v
@@ -20,6 +20,9 @@ Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits.
 Require Archi.
 
+(** Ignore Hint Rewrite global attribute for Coq 8.13 *)
+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:

diff --git a/zlist/list_solver.v b/zlist/list_solver.v
@@ -8,6 +8,9 @@ Require Export VST.zlist.sublist.
 Import SublistInternalLib.
 Require Export VST.zlist.Zlength_solver.
 
+(** Ignore Hint Rewrite global attribute for Coq 8.13 *)
+Set Warnings "-unsupported-attributes".
+
 (** This file provides a almost-complete solver for list with concatenation.
   Its core symbols include:
     Zlength