diff --git a/_CoqProject b/_CoqProject
index 39b0f345f5c1c37585a94c2d6fe9763a2398bbf6..d91caa8feace58cb818fef3a08e473da6acc56ad 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,12 +1,9 @@
 -Q theories lrust
 # We sometimes want to locally override notation, 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/lifetime/model/definitions.v
 theories/lifetime/model/faking.v
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 06af6e4e67fa7e33d049c60ee9caa742dd811201..d4f4241087e04e08f476d3c767eacab40dc2bf7e 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -9,6 +9,7 @@ Open Scope Z_scope.
 Definition block : Set := positive.
 Definition loc : Set := block * Z.
 
+Declare Scope loc_scope.
 Bind Scope loc_scope with loc.
 Delimit Scope loc_scope with L.
 Open Scope loc_scope.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index d4f5d697b4f140a33ebcb78810877b23756bfc57..000abf66f7e241aa228e2cd83101d5f81c54f23e 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -94,6 +94,6 @@ Notation "'letcall:' x := f args 'in' e" :=
    we would even want them to print in general.
    TODO: Introduce a Definition. *)
 Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
-  (only parsing, at level 80, format "e1  <-{Σ  i }  ()" ) : expr_scope.
+  (only parsing, at level 80) : expr_scope.
 Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
   (at level 80, format "e1 <-{Σ  i }  e2") : expr_scope.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f8b22f40d0e386deecd0204466408d4ef4bd157d..f28c75b5ac462ee47f3a42f81341c211348c57dc 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -8,6 +8,7 @@ Set Default Proof Using "Type".
 Definition elctx_elt : Type := lft * lft.
 Notation elctx := (list elctx_elt).
 
+Declare Scope lrust_elctx_scope.
 Delimit Scope lrust_elctx_scope with EL.
 (* We need to define [elctx] and [llctx] as notations to make eauto
    work. But then, Coq is not able to bind them to their
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 905b05c4d1e21c9495c7e1feb38694402d596990..0d9bff1f825bdc43683159d655301ec68f3f86a0 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -144,6 +144,7 @@ Qed.
 
 Coercion ty_of_st : simple_type >-> type.
 
+Declare Scope lrust_type_scope.
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.