diff --git a/_CoqProject b/_CoqProject
index 5b36787dbdbad575aa0dd481bd45cfa2d313a7dc..271fa04fa6b711f142da368f52c03fac60319ae2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,8 @@
 -arg -w -arg -convert_concl_no_check
 # non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
 -arg -w -arg -redundant-canonical-projection
+# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
+-arg -w -arg -ambiguous-paths
 
 theories/prelude/ctx_subst.v
 theories/prelude/properness.v
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 09477ad1b6054d98ca49a0861fd1faba54739283..b884eb7052ba2fe5a0950ec011fde3749352bbd2 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -7,6 +7,12 @@ From iris.algebra Require Import csum agree excl.
 From reloc Require Export reloc.
 From reloc.lib Require Export lock counter Y.
 
+Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
+Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
+Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
+Proof. solve_inG. Qed.
+
 Section proofs.
   Context `{relocG Σ}.
 
@@ -35,12 +41,6 @@ Section proofs.
       rel_values.
   Qed.
 
-  Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
-  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
-  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
-  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
-  Proof. solve_inG. Qed.
-
   Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
   Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
   Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 057ce90f36ee59cf9ea84e63bc85f16d2eda3c96..ffa2377b77b697a14ee8fcb05fe5415c823ade02 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -18,6 +18,7 @@ Record lrel Σ := LRel {
 }.
 Arguments LRel {_} _%I {_}.
 Arguments lrel_car {_} _ _ _ : simpl never.
+Declare Scope lrel_scope.
 Bind Scope lrel_scope with lrel.
 Delimit Scope lrel_scope with lrel.
 Existing Instance lrel_persistent.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2849bfdef781cecedca5298ca345a9da2f8e136a..3b7be1f8f26551711714f0adbf7376404aa0e65d 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -14,11 +14,11 @@ Section rules.
   Implicit Types v : val.
   Implicit Types l : loc.
 
-  Local Hint Resolve tpool_lookup.
-  Local Hint Resolve tpool_lookup_Some.
-  Local Hint Resolve to_tpool_insert.
-  Local Hint Resolve to_tpool_insert'.
-  Local Hint Resolve tpool_singleton_included.
+  Local Hint Resolve tpool_lookup : core.
+  Local Hint Resolve tpool_lookup_Some : core.
+  Local Hint Resolve to_tpool_insert : core.
+  Local Hint Resolve to_tpool_insert' : core.
+  Local Hint Resolve tpool_singleton_included : core.
 
   (** * Aux. lemmas *)
   Lemma step_insert K tp j e σ κ e' σ' efs :
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 862224036833b2e89cb6ddf4c4ad3fbbe4321904..430ac9f2e638e06f6942b647a308dd1f5e790fbd 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -11,7 +11,7 @@ From Autosubst Require Import Autosubst.
 Section fundamental.
   Context `{relocG Σ}.
   Implicit Types Δ : listO (lrelC Σ).
-  Hint Resolve to_of_val.
+  Hint Resolve to_of_val : core.
 
   Local Ltac intro_clause := progress (iIntros (vs) "#Hvs /=").
   Local Ltac intro_clause' := progress (iIntros (?) "? /=").
diff --git a/theories/typing/types.v b/theories/typing/types.v
index ecc67ba81b00e8d81581c34e45e7b5384377b592..d5722e9984748ca279dbbb1a313403f4d0a2ac13 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -51,6 +51,7 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
   | _ => None
   end.
 
+Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
 Infix "*" := TProd : FType_scope.