diff options
| author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2022-07-05 11:27:40 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-07-05 11:27:40 +0200 |
| commit | df076edfe673069decf9e8b0dc5f3b7941796060 (patch) | |
| tree | 89faeb06d3756c406425c78b7fc597504ad8dd73 | |
| parent | e4bba56773fc059e592f72a49b1010f53f3126f0 (diff) | |
| download | compcert-df076edfe673069decf9e8b0dc5f3b7941796060.tar.gz compcert-df076edfe673069decf9e8b0dc5f3b7941796060.zip | |
Add [#global] qualifier on Hint Rewrite (#439)
Adapt w.r.t. coq/coq#16004.
| -rw-r--r-- | common/Events.v | 4 | ||||
| -rw-r--r-- | lib/Integers.v | 8 |
2 files changed, 12 insertions, 0 deletions
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: |