upgrade to coq 8.14.0

.gitlab-ci.yml

@@ -6,7 +6,7 @@ stages:
 variables:
   # dune takes care of parallelization itself and does not like running in parallel
   CPU_CORES: "1"
-  MAKE_TARGET: "all_with_examples"
+  MAKE_TARGET: "ci"
   OCAML: "ocaml-base-compiler.4.07.1"
 
 .template: &template
@@ -30,10 +30,10 @@ variables:
   - api
 
 ## Build jobs
-build-coq.8.13.2-timing:
+build-coq.8.14.0-timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.2   cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
+    OPAM_PINS: "coq version 8.14.0   cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
     DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   only:
@@ -43,10 +43,10 @@ build-coq.8.13.2-timing:
   tags:
   - fp-timing
 
-build-coq.8.13.2:
+build-coq.8.14.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.2   cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
+    OPAM_PINS: "coq version 8.14.0   cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
     DENY_WARNINGS: "1"
   only:
   - /^ci/@iris/refinedc
@@ -54,7 +54,7 @@ build-coq.8.13.2:
 trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
+    OPAM_PINS: "coq version 8.14.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
   except:
   only:
   - triggers

Makefile

@@ -6,6 +6,10 @@ all_with_examples: generate_all
 	@dune build --display short
 .PHONY: all_with_examples
 
+ci: restore_dune_project all_with_examples
+	@true
+.PHONY: ci_all
+
 install:
 	@dune install
 .PHONY: install
@@ -37,9 +41,18 @@ clean: clean_generated
 .PHONY: clean
 
 builddep-opamfiles: builddep/refinedc-builddep.opam
+	@echo "# Renaming dune-project to work around coq#15044"
+	@mv dune-project dune-project.tmp
 	@true
 .PHONY: builddep-opamfiles
 
+restore_dune_project:
+	@if [ -f dune-project.tmp ] && ! [ -e dune-project ]; then \
+		echo "# Renaming dune-project back";\
+		mv dune-project.tmp dune-project;\
+	fi
+.PHONY: restore_dune_project
+
 # Create a virtual Opam package with the same deps as RefinedC, but no
 # build. Uses a very ugly hack to use sed for removing the last 4
 # lines since head -n -4 does not work on MacOS
@@ -54,8 +67,12 @@ builddep/refinedc-builddep.opam: refinedc.opam Makefile
 #  2) they will remain satisfied even if other packages are updated/installed,
 #  3) we do not have to pin the RefinedC package itself (which takes time).
 builddep: builddep/refinedc-builddep.opam
+	@echo "# Renaming dune-project to work around coq#15044"
+	@mv dune-project dune-project.tmp
 	@echo "# Installing package $^."
 	@opam install $(OPAMFLAGS) $^
+	@echo "# Renaming dune-project back"
+	@mv dune-project.tmp dune-project
 .PHONY: builddep
 
 # FIXME

dune-project

-(lang dune 2.7)
+(lang dune 2.9)
 (name refinedc)
-(using coq 0.2)
+(using coq 0.3)

examples/proofs/quick_sort/quick_sort_lemmas.v

@@ -61,13 +61,13 @@ Inductive range : Type :=
   | ei : nat → nat → range (* (l, r] *)
   .
 
-Instance range_elem_of : ElemOf nat range := λ i I,
+Global Instance range_elem_of : ElemOf nat range := λ i I,
   match I with
   | ie l r => l ≤ i ∧ i < r
   | ei l r => l < i ∧ i ≤ r
   end.
 
-Instance range_elem_of_decision (i : nat) (I : range) : Decision (i ∈ I).
+Global Instance range_elem_of_decision (i : nat) (I : range) : Decision (i ∈ I).
 Proof.
   destruct I as [l r | l r].
   - destruct (decide (l ≤ i ∧ i < r)); by [ left | right ].

examples/proofs/wrapping_add/wrapping_def.v

@@ -7,7 +7,7 @@ Definition WrappingAdd (it1 it2 : int_type) (es : list expr) : expr :=
   | _ => Val VOID
   end%E.
 
-Program Instance WrappingAdd_wf it1 it2 : MacroWfSubst (WrappingAdd it1 it2).
+Global Program Instance WrappingAdd_wf it1 it2 : MacroWfSubst (WrappingAdd it1 it2).
 Next Obligation. move => ???? [|?[|?[|??]]]//. Qed.
 
 Typeclasses Opaque WrappingAdd.

linux/pkvm/proofs/early_alloc/instances.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 Lemma shift_12_eq_mul_4096 n :
   (n ≪ 12) = n * 4096.
 Proof. by rewrite Z.shiftl_mul_pow2. Qed.
-Hint Rewrite shift_12_eq_mul_4096 : lithium_rewrite.
+#[export] Hint Rewrite shift_12_eq_mul_4096 : lithium_rewrite.
 
 Lemma ly_size_PAGES i : ly_size (PAGES i) = (i * Z.to_nat PAGE_SIZE)%nat.
 Proof. by rewrite /PAGES /ly_with_align /ly_size. Qed.
@@ -38,12 +38,12 @@ Proof. rewrite !ly_size_PAGES. lia. Qed.
 Typeclasses Opaque PAGES.
 Global Opaque PAGES.
 
-Hint Rewrite ly_size_ly_offset : lithium_rewrite.
-Hint Rewrite ly_size_PAGES_sub : lithium_rewrite.
-Hint Rewrite ly_size_PAGES : lithium_rewrite.
-Hint Rewrite ly_offset_PAGES : lithium_rewrite.
+#[export] Hint Rewrite ly_size_ly_offset : lithium_rewrite.
+#[export] Hint Rewrite ly_size_PAGES_sub : lithium_rewrite.
+#[export] Hint Rewrite ly_size_PAGES : lithium_rewrite.
+#[export] Hint Rewrite ly_offset_PAGES : lithium_rewrite.
 
-Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
-Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
-Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
-Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.

linux/pkvm/proofs/spinlock/spinlock_def.v

@@ -25,7 +25,7 @@ Class spinlockG Σ := SpinLockG {
 Definition spinlockΣ : gFunctors :=
   #[GFunctor (constRF (gmapR Z (exclR unitO)));
     GFunctor (constRF (excl_authR ZO))].
-Instance subG_spinlockG {Σ} : subG spinlockΣ Σ → spinlockG Σ.
+Global Instance subG_spinlockG {Σ} : subG spinlockΣ Σ → spinlockG Σ.
 Proof. solve_inG. Qed.
 
 Section type.

refinedc.opam

@@ -16,9 +16,9 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
 
 depends: [
-  "coq" { (>= "8.13.2" & < "8.15~") }
+  "coq" { (>= "8.14.0" & < "8.15~") }
   "coq-iris" { (= "dev.2021-09-13.0.6575260a") | (= "dev") }
-  "dune" {>= "2.7.0"}
+  "dune" {>= "2.9.1"}
   "cerberus" {= "~dev"}
   "cmdliner" {>= "1.0.4"}
   "earley" {= "3.0.0"}

theories/lang/bitfield.v

@@ -277,27 +277,27 @@ Qed.
 (* rewrite & simpl rules *)
 Create HintDb bitfield_rewrite discriminated.
 
-Hint Rewrite bf_land_nil : bitfield_rewrite.
-Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite.
-Hint Rewrite bf_land_mask_flip using can_solve_tac : bitfield_rewrite.
-
-Hint Rewrite bf_lor_nil_l : bitfield_rewrite.
-Hint Rewrite bf_lor_nil_r : bitfield_rewrite.
-Hint Rewrite bf_lor_update using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite.
-Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite.
-
-Hint Rewrite bf_slice_nil : bitfield_rewrite.
-Hint Rewrite bf_slice_cons using can_solve_tac : bitfield_rewrite.
-Hint Rewrite bf_slice_cons_ne using lia : bitfield_rewrite.
-
-Hint Rewrite bf_update_nil : bitfield_rewrite.
-Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
-Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_land_nil : bitfield_rewrite.
+#[export] Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite.
+#[export] Hint Rewrite bf_land_mask_flip using can_solve_tac : bitfield_rewrite.
+
+#[export] Hint Rewrite bf_lor_nil_l : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_nil_r : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_update using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite.
+
+#[export] Hint Rewrite bf_slice_nil : bitfield_rewrite.
+#[export] Hint Rewrite bf_slice_cons using can_solve_tac : bitfield_rewrite.
+#[export] Hint Rewrite bf_slice_cons_ne using lia : bitfield_rewrite.
+
+#[export] Hint Rewrite bf_update_nil : bitfield_rewrite.
+#[export] Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
+#[export] Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
 
 Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
 Typeclasses Opaque normalize_bitfield.

theories/lang/byte.v

@@ -17,7 +17,7 @@ Record byte :=
 Program Definition byte0 : byte := {| byte_val := 0; |}.
 Next Obligation. done. Qed.
 
-Instance byte_eq_dec : EqDecision byte.
+#[export] Instance byte_eq_dec : EqDecision byte.
 Proof.
   move => [b1 H1] [b2 H2]. destruct (decide (b1 = b2)) as [->|].
   - left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.

theories/lang/heap.v

@@ -188,7 +188,7 @@ Qed.
 (** An allocation can either be a stack allocation or a heap allocation. *)
 Inductive alloc_kind : Set :=
   | HeapAlloc
-  | StackAlloc 
+  | StackAlloc
   | GlobalAlloc.
 
 Record allocation :=
@@ -222,7 +222,7 @@ memory (e.g., does not contain NULL). *)
 Definition allocation_in_range (al : allocation) : Prop :=
   min_alloc_start ≤ al.(al_start) ∧ al_end al ≤ max_alloc_end.
 
-Instance elem_of_alloc : ElemOf addr allocation :=
+Global Instance elem_of_alloc : ElemOf addr allocation :=
   λ a al, al.(al_start) ≤ a < al_end al.
 
 (** ** Representation of the state of the heap and allocation operations. *)

theories/lang/lang.v

@@ -669,7 +669,7 @@ Lemma val_stuck e1 σ1 κ e2 σ2 ef :
   runtime_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1 => //. revert select (expr_step _ _ _ _ _ _). by destruct 1. Qed.
 
-Instance fill_item_inj Ki : Inj (=) (=) (lang_fill_item Ki).
+Global Instance fill_item_inj Ki : Inj (=) (=) (lang_fill_item Ki).
 Proof. destruct Ki as [E|E ?]; destruct E; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma fill_item_val Ki e :
@@ -705,15 +705,15 @@ Canonical Structure c_lang := LanguageOfEctx c_ectx_lang.
 
 (** * Useful instances and canonical structures *)
 
-Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
-Instance val_inhabited : Inhabited val := _.
-Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
-Instance stmt_inhabited : Inhabited stmt := populate (Goto "a").
-Instance function_inhabited : Inhabited function :=
+Global Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
+Global Instance val_inhabited : Inhabited val := _.
+Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
+Global Instance stmt_inhabited : Inhabited stmt := populate (Goto "a").
+Global Instance function_inhabited : Inhabited function :=
   populate {| f_args := []; f_local_vars := []; f_code := ∅; f_init := "" |}.
-Instance heap_state_inhabited : Inhabited heap_state :=
+Global Instance heap_state_inhabited : Inhabited heap_state :=
   populate {| hs_heap := inhabitant; hs_allocs := inhabitant; |}.
-Instance state_inhabited : Inhabited state :=
+Global Instance state_inhabited : Inhabited state :=
   populate {| st_heap := inhabitant; st_fntbl := inhabitant; |}.
 
 Canonical Structure mbyteO := leibnizO mbyte.

theories/lang/lifting.v

@@ -11,7 +11,7 @@ Class refinedcG Σ := RefinedCG {
   refinedcG_gen_heapG :> heapG Σ
 }.
 
-Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
+Global Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
   iris_invGS := refinedcG_invG;
   state_interp σ κs _ _ := state_ctx σ;
   fork_post _ := True%I;
@@ -20,7 +20,7 @@ Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
 }.
 Global Opaque iris_invGS.
 
-Instance into_val_val v : IntoVal (to_rtexpr (Val v)) v.
+Global Instance into_val_val v : IntoVal (to_rtexpr (Val v)) v.
 Proof. done. Qed.
 
 Global Instance wp_expr_wp `{!refinedcG Σ} : Wp (iProp Σ) expr val stuckness :=
@@ -36,13 +36,13 @@ Local Ltac solve_atomic :=
     [inversion 1; unfold coerce_rtexpr in *; simplify_eq; inv_expr_step; naive_solver
     |unfold coerce_rtexpr in *;apply ectxi_language_sub_redexes_are_values; intros [[]|[]] **; naive_solver].
 
-Instance cas_atomic s ot (v1 v2 v3 : val) : Atomic s (coerce_rtexpr (CAS ot v1 v2 v3)).
+Global Instance cas_atomic s ot (v1 v2 v3 : val) : Atomic s (coerce_rtexpr (CAS ot v1 v2 v3)).
 Proof. solve_atomic. Qed.
-Instance skipe_atomic s (v : val) : Atomic s (coerce_rtexpr (SkipE v)).
+Global Instance skipe_atomic s (v : val) : Atomic s (coerce_rtexpr (SkipE v)).
 Proof. solve_atomic. Qed.
-Instance deref_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Deref ScOrd ly l)).
+Global Instance deref_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Deref ScOrd ly l)).
 Proof. solve_atomic. Qed.
-Instance use_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Use ScOrd ly l)).
+Global Instance use_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Use ScOrd ly l)).
 Proof. solve_atomic. Qed.
 
 (*** General lifting lemmas *)

theories/lang/loc.v

@@ -201,5 +201,5 @@ Proof.
   apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
 Qed.
 
-Instance aligned_to_dec l n : Decision (l `aligned_to` n).
+#[export] Instance aligned_to_dec l n : Decision (l `aligned_to` n).
 Proof. apply Znumtheory.Zdivide_dec. Qed.

theories/lang/val.v

@@ -10,7 +10,7 @@ Inductive mbyte : Set :=
 | MPtrFrag (l : loc) (n : nat) (** Fragment [n] for location [l]. *)
 | MPoison.
 
-Instance mbyte_dec_eq : EqDecision mbyte.
+#[export] Instance mbyte_dec_eq : EqDecision mbyte.
 Proof. solve_decision. Qed.
 
 Program Definition mbyte_to_byte (mb : mbyte) : option (byte * option alloc_id) :=

theories/lithium/Z_bitblast.v

@@ -10,7 +10,7 @@ Local Open Scope Z_scope.
 
 Create HintDb simplify_bool_eq_db discriminated.
 
-Hint Rewrite
+#[export] Hint Rewrite
   Bool.andb_false_r
   Bool.andb_true_r
   Bool.andb_false_l
@@ -29,7 +29,7 @@ Ltac simplify_bool_eq := autorewrite with simplify_bool_eq_db.
 
 Create HintDb simplify_index_db discriminated.
 
-Hint Rewrite
+#[export] Hint Rewrite
   Z.sub_add
   Z.add_simpl_r
   : simplify_index_db.
@@ -48,7 +48,7 @@ Qed.
 
 Create HintDb rewrite_bits_db discriminated.
 
-Hint Rewrite
+#[export] Hint Rewrite
   (* 0 *)
   Z.bits_0
   (* 1 *)

theories/lithium/normalize.v

@@ -6,31 +6,31 @@ Create HintDb lithium_rewrite discriminated.
 Ltac normalize_autorewrite :=
   autorewrite with lithium_rewrite; exact: eq_refl.
 
-Hint Rewrite @drop_0 @take_ge using can_solve_tac : lithium_rewrite.
-Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : lithium_rewrite.
-Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : lithium_rewrite.
-Hint Rewrite <- @fmap_take @fmap_drop : lithium_rewrite.
-Hint Rewrite @list_insert_fold : lithium_rewrite.
-Hint Rewrite @list_insert_insert : lithium_rewrite.
-Hint Rewrite @drop_drop : lithium_rewrite.
-Hint Rewrite @tail_replicate @take_replicate @drop_replicate : lithium_rewrite.
-Hint Rewrite <- @app_assoc @cons_middle : lithium_rewrite.
-Hint Rewrite @app_nil_r @rev_involutive : lithium_rewrite.
-Hint Rewrite <- @list_fmap_insert : lithium_rewrite.
-Hint Rewrite <- minus_n_O plus_n_O minus_n_n : lithium_rewrite.
-Hint Rewrite Nat2Z.id : lithium_rewrite.
-Hint Rewrite Z2Nat.inj_mul Z2Nat.inj_sub Z2Nat.id using can_solve_tac : lithium_rewrite.
-Hint Rewrite Nat.succ_pred_pos using can_solve_tac : lithium_rewrite.
-Hint Rewrite Nat.add_assoc Nat.min_id : lithium_rewrite.
-Hint Rewrite Z.quot_mul using can_solve_tac : lithium_rewrite.
-Hint Rewrite <-Nat.mul_sub_distr_r Z.mul_add_distr_r Z.mul_sub_distr_r : lithium_rewrite.
-Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : lithium_rewrite.
-Hint Rewrite @bool_decide_eq_true_2 @bool_decide_eq_false_2 using fast_done : lithium_rewrite.
-Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : lithium_rewrite.
-Hint Rewrite keep_factor2_min_1 keep_factor2_twice : lithium_rewrite.
+#[export] Hint Rewrite @drop_0 @take_ge using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : lithium_rewrite.
+#[export] Hint Rewrite <- @fmap_take @fmap_drop : lithium_rewrite.
+#[export] Hint Rewrite @list_insert_fold : lithium_rewrite.
+#[export] Hint Rewrite @list_insert_insert : lithium_rewrite.
+#[export] Hint Rewrite @drop_drop : lithium_rewrite.
+#[export] Hint Rewrite @tail_replicate @take_replicate @drop_replicate : lithium_rewrite.
+#[export] Hint Rewrite <- @app_assoc @cons_middle : lithium_rewrite.
+#[export] Hint Rewrite @app_nil_r @rev_involutive : lithium_rewrite.
+#[export] Hint Rewrite <- @list_fmap_insert : lithium_rewrite.
+#[export] Hint Rewrite <- minus_n_O plus_n_O minus_n_n : lithium_rewrite.
+#[export] Hint Rewrite Nat2Z.id : lithium_rewrite.
+#[export] Hint Rewrite Z2Nat.inj_mul Z2Nat.inj_sub Z2Nat.id using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite Nat.succ_pred_pos using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite Nat.add_assoc Nat.min_id : lithium_rewrite.
+#[export] Hint Rewrite Z.quot_mul using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite <-Nat.mul_sub_distr_r Z.mul_add_distr_r Z.mul_sub_distr_r : lithium_rewrite.
+#[export] Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : lithium_rewrite.
+#[export] Hint Rewrite @bool_decide_eq_true_2 @bool_decide_eq_false_2 using fast_done : lithium_rewrite.
+#[export] Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : lithium_rewrite.
+#[export] Hint Rewrite keep_factor2_min_1 keep_factor2_twice : lithium_rewrite.
 
 Local Definition lookup_insert_gmap A K `{Countable K} := lookup_insert (M := gmap K) (A := A).
-Hint Rewrite lookup_insert_gmap : lithium_rewrite.
+#[export] Hint Rewrite lookup_insert_gmap : lithium_rewrite.
 
 (** * Second version of normalization based on typeclasses *)
 Class NormalizeWalk {A} (progress : bool) (a b : A) : Prop := normalize_walk: a = b.

theories/typing/adequacy.v

@@ -21,7 +21,7 @@ Definition typeΣ : gFunctors :=
    ghost_mapΣ alloc_id (Z * nat * alloc_kind);
    ghost_mapΣ alloc_id bool;
    ghost_mapΣ addr function].
-Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Global Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
 Proof. solve_inG. Qed.
 
 Definition initial_prog (main : loc) : runtime_expr :=

theories/typing/automation/loc_eq.v

@@ -11,13 +11,13 @@ extend with more rewriting rules. *)
 Create HintDb refinedc_loc_eq_rewrite discriminated.
 
 (** Rules to inject [nat] operations in to [Z]. *)
-Hint Rewrite Nat2Z.inj_mul : refinedc_loc_eq_rewrite.
-Hint Rewrite Nat2Z.inj_add : refinedc_loc_eq_rewrite.
-Hint Rewrite Nat2Z.inj_sub using lia : refinedc_loc_eq_rewrite.
-Hint Rewrite Z2Nat.id using lia : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite Nat2Z.inj_mul : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite Nat2Z.inj_add : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite Nat2Z.inj_sub using lia : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite Z2Nat.id using lia : refinedc_loc_eq_rewrite.
 
 (** Rule to eliminate [Z.shiftl]. *)
-Hint Rewrite Z.shiftl_mul_pow2 using lia : refinedc_loc_eq_rewrite.
+#[export] Hint Rewrite Z.shiftl_mul_pow2 using lia : refinedc_loc_eq_rewrite.
 
 (** * Tactics *)
 

theories/typing/automation/normalize.v

 From refinedc.typing Require Import type.
 From refinedc.lithium Require Export normalize.
 
-Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : lithium_rewrite.
-Hint Rewrite ly_size_ly_set_size ly_size_ly_with_align : lithium_rewrite.
+#[export] Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : lithium_rewrite.
+#[export] Hint Rewrite ly_size_ly_set_size ly_size_ly_with_align : lithium_rewrite.
 
 (* The following lemma is a problem with Keyed Unification as it
 unfolds e.g. layout_of *)