diff --git a/_CoqProject b/_CoqProject
index aeb000f4f9688fe2d061808041c8fbcba5b6efe8..5a92de86d06e0a538193d125b74cf7d008b983ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,12 +2,9 @@
 # We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
 # is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
-# Non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294)
 -arg -w -arg -redundant-canonical-projection
-# change_no_check does not exist yet in 8.9.
--arg -w -arg -convert_concl_no_check
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index d1102210d63566e5a19c2ccff9ea358835afedde..a05c9a71651d593291cc47484a3048df123c2182 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 From iris.bi Require Import ascii.
 
 Set Default Proof Using "Type".
-Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
+Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
 
 Section base_logic_tests.
   Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 5d7b84d2a262de98eb6a89679b2a87fe643a026d..f90d0db21115ccfa291236847d8d133566dcd076 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
-Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
+Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
 
 Section tests.
   Context {I : biIndex} {PROP : bi}.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 979462cac1609f9e534186d4d825ff18c76c238e..b56fade14a8b34408d61adcc1aca5ca15e336e53 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -794,6 +794,7 @@ Record rFunctor := RFunctor {
 Existing Instances rFunctor_map_ne rFunctor_mor.
 Instance: Params (@rFunctor_map) 9 := {}.
 
+Declare Scope rFunctor_scope.
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
@@ -866,6 +867,7 @@ Record urFunctor := URFunctor {
 Existing Instances urFunctor_map_ne urFunctor_mor.
 Instance: Params (@urFunctor_map) 9 := {}.
 
+Declare Scope urFunctor_scope.
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 71c86a043d5874a7bd7d4e71962d43b1fbfec49b..c96fc87bda2ab76bf8934562d081921faeeb9fcb 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -704,6 +704,7 @@ Record oFunctor := OFunctor {
 Existing Instance oFunctor_map_ne.
 Instance: Params (@oFunctor_map) 9 := {}.
 
+Declare Scope oFunctor_scope.
 Delimit Scope oFunctor_scope with OF.
 Bind Scope oFunctor_scope with oFunctor.
 
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index ee70c6117cc62d83c7739ad312d58ffa046beef4..6df3cd65d2583a77bddd51459d597b446ae4bc13 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -26,6 +26,7 @@ Record monPred :=
             monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
 Local Existing Instance monPred_mono.
 
+Declare Scope monPred.
 Bind Scope monPred with bi.
 
 Implicit Types P Q : monPred.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 99599c3beb55ddbd5b91094c9b3349dbd87ff632..d67cc7f8948db4340dd8db5c36071cccb6ad1f2a 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -179,4 +179,5 @@ Reserved Notation "'[∗' 'mset]' x ∈ X , P"
    format "[∗  mset]  x  ∈  X ,  P").
 
 (** Define the scope *)
+Declare Scope bi_scope.
 Delimit Scope bi_scope with I.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 0948a57f9af86b7fa31d308d029f6e938f4c61d9..6e60bbd0a8928ab6301a18cfd530f0c48493b297 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -2,9 +2,6 @@ From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang.
 Set Default Proof Using "Type".
 
-Delimit Scope expr_scope with E.
-Delimit Scope val_scope with V.
-
 (** Coercions to make programs easier to type. *)
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 2fa0f289e93326d297fe160bdcf9ee912ed3ad36..6999e0163729febb50529156bf16a54670774044 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -27,9 +27,13 @@ Structure language := Language {
   prim_step : expr → state → list observation → expr → state → list expr → Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
+
+Declare Scope expr_scope.
 Delimit Scope expr_scope with E.
-Delimit Scope val_scope with V.
 Bind Scope expr_scope with expr.
+
+Declare Scope val_scope.
+Delimit Scope val_scope with V.
 Bind Scope val_scope with val.
 
 Arguments Language {_ _ _ _ _ _ _} _.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index e11fb4bce3197ec00e4a2cf7852487575d19a944..5e99d04ed75b0ef2298682bc1271d25fe854e541 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -234,7 +234,7 @@ an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q
 and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This
 way, [iFresh] can simply be implemented by changing the goal from
 [envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q]
-using the tactic [convert_concl_no_check]. This way, the generated proof term
+using the tactic [change_no_check]. This way, the generated proof term
 contains no additional steps for changing the counter.
 
 For all definitions below, we first define a version that take the two contexts
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 1accdff035de9233d7fa2d2238f0b64d57bb0389..203f53c92d97d63f7900982c39036b169aa9d54c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -123,7 +123,7 @@ Ltac iFresh :=
     lazymatch goal with
     | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
       let c' := eval vm_compute in (Pos.succ c) in
-      convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
+      change_no_check (envs_entails (Envs Δp Δs c') Q)
     end in
   constr:(IAnon c).
 
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index f9a53fb58c747793bc5d38d551e6bc8b2c359789..0025dc12ea87204306b49c36d7e45303a6204741 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -2,6 +2,7 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import coq_tactics environments.
 Set Default Proof Using "Type".
 
+Declare Scope proof_scope.
 Delimit Scope proof_scope with env.
 Arguments Envs _ _%proof_scope _%proof_scope _.
 Arguments Enil {_}.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index b5af9b8183374a1f64cfce6f11768c1d361c3cd2..c9d616778b9208c260a161160b1c5faeaae43375 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -22,9 +22,9 @@ Declare Reduction pm_eval := cbv [
 Ltac pm_eval t :=
   eval pm_eval in t.
 Ltac pm_reduce :=
-  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  (* Use [change_no_check] instead of [change] to avoid performing the
   conversion check twice. *)
-  match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
+  match goal with |- ?u => let v := pm_eval u in change_no_check v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
 (** Called by many tactics for redexes that are created by instantiation.
@@ -38,6 +38,6 @@ Declare Reduction pm_prettify := cbn [
   bi_tforall bi_texist
 ].
 Ltac pm_prettify :=
-  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  (* Use [change_no_check] instead of [change] to avoid performing the
   conversion check twice. *)
-  match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
+  match goal with |- ?u => let v := eval pm_prettify in u in change_no_check v end.
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index d1538b871aa6d7cebd53c48d23ca56b420bab475..1ea1bde1fe2301efd5a6911d36369f4798379847 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -10,6 +10,8 @@ Record siProp := SiProp {
 }.
 Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.
+
+Declare Scope siProp_scope.
 Delimit Scope siProp_scope with SI.
 Bind Scope siProp_scope with siProp.