diff --git a/theories/logrel/F_mu/logrel.v b/theories/logrel/F_mu/logrel.v
index 4c2450e19b74f049db2e3fefc7c03a74d0faa984..ff721cbbc3688bc2bfe676b557e8440972f992cf 100644
--- a/theories/logrel/F_mu/logrel.v
+++ b/theories/logrel/F_mu/logrel.v
@@ -88,7 +88,7 @@ Section logrel.
     env_Persistent Δ → Persistent (ctx_lookup x Δ v).
   Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
   Global Instance interp_persistent τ Δ v :
-    env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v) := _.
+    env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v).
   Proof.
     revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
     rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
diff --git a/theories/logrel/F_mu_ref_conc/examples/lock.v b/theories/logrel/F_mu_ref_conc/examples/lock.v
index 562d2d45f0b6914886cd96f267c92a098981f499..ba8a8a915a22a1246bca5e3a661b90ffd3500101 100644
--- a/theories/logrel/F_mu_ref_conc/examples/lock.v
+++ b/theories/logrel/F_mu_ref_conc/examples/lock.v
@@ -159,7 +159,7 @@ Section proof.
   Global Opaque with_lock.
 End proof.
 
-Global Hint Rewrite newlock_closed : autosubst.
-Global Hint Rewrite acquire_closed : autosubst.
-Global Hint Rewrite release_closed : autosubst.
-Global Hint Rewrite with_lock_subst : autosubst.
+Hint Rewrite newlock_closed : autosubst.
+Hint Rewrite acquire_closed : autosubst.
+Hint Rewrite release_closed : autosubst.
+Hint Rewrite with_lock_subst : autosubst.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
index 3309b710afe2850da1185b6e5dc18ac7519bb489..d6a5b42bccd894d4c07f071b3cca55856a6e9faa 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
@@ -79,7 +79,7 @@ Section CG_Stack.
   Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
   Proof. unfold CG_push; asimpl; trivial. Qed.
 
-  Global Hint Rewrite CG_push_subst : autosubst.
+  Hint Rewrite CG_push_subst : autosubst.
 
   Lemma steps_CG_push E ρ j K st v w :
     nclose specN ⊆ E →
@@ -451,13 +451,13 @@ Section CG_Stack.
 
 End CG_Stack.
 
-Global Hint Rewrite CG_push_subst : autosubst.
-Global Hint Rewrite CG_locked_push_subst : autosubst.
-Global Hint Rewrite CG_locked_pop_subst : autosubst.
-Global Hint Rewrite CG_pop_subst : autosubst.
-Global Hint Rewrite CG_locked_pop_subst : autosubst.
-Global Hint Rewrite CG_snap_subst : autosubst.
-Global Hint Rewrite CG_iter_subst : autosubst.
-Global Hint Rewrite CG_snap_iter_subst : autosubst.
-Global Hint Rewrite CG_stack_body_subst : autosubst.
-Global Hint Rewrite CG_stack_closed : autosubst.
+Hint Rewrite CG_push_subst : autosubst.
+Hint Rewrite CG_locked_push_subst : autosubst.
+Hint Rewrite CG_locked_pop_subst : autosubst.
+Hint Rewrite CG_pop_subst : autosubst.
+Hint Rewrite CG_locked_pop_subst : autosubst.
+Hint Rewrite CG_snap_subst : autosubst.
+Hint Rewrite CG_iter_subst : autosubst.
+Hint Rewrite CG_snap_iter_subst : autosubst.
+Hint Rewrite CG_stack_body_subst : autosubst.
+Hint Rewrite CG_stack_closed : autosubst.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
index 15e1073b08d5d9941f62c8bed9bb1921ea1d7501..2b3d4661fafb9e0013478ca0e16122d0ded13b0b 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
@@ -329,9 +329,9 @@ Section FG_stack.
 
 End FG_stack.
 
-Global Hint Rewrite FG_push_subst : autosubst.
-Global Hint Rewrite FG_pop_subst : autosubst.
-Global Hint Rewrite FG_iter_subst : autosubst.
-Global Hint Rewrite FG_read_iter_subst : autosubst.
-Global Hint Rewrite FG_stack_body_subst : autosubst.
-Global Hint Rewrite FG_stack_closed : autosubst.
+Hint Rewrite FG_push_subst : autosubst.
+Hint Rewrite FG_pop_subst : autosubst.
+Hint Rewrite FG_iter_subst : autosubst.
+Hint Rewrite FG_read_iter_subst : autosubst.
+Hint Rewrite FG_stack_body_subst : autosubst.
+Hint Rewrite FG_stack_closed : autosubst.