diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 26e177f00546b0ffc97f56ab4de017e462e9adf1..1dad2e95a2de7c538c12dda355e038967e58b04e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,10 +27,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.12.dev:
+build-coq.8.12.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.dev"
+    OPAM_PINS: "coq version 8.12.0"
 
 build-coq.8.11.2:
   <<: *template
diff --git a/README.md b/README.md
index d566a24e9e5c5d0b1c88bfae56972f83ffc2d89c..9c3f4160912b7c2abb6a9a694199415be141e10c 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying RBrlx.
 
 This version is known to compile with:
 
- - Coq 8.11.2
+ - Coq 8.11.2 / 8.12.0
  - A development version of [GPFSL].
 
 The easiest way to install the correct versions of the dependencies is through
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 055af49659eb57060439edbfcb00828fabab66b8..73c7c8dffee0c9c93955d5fe778723cf7d0348df 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 b4fe9a2dd59cf602ba110d0465c2cfc9218e7fdc..b36995654305cf3b24e7b866d68d59f4d93a4e07 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -147,6 +147,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.