test Coq 8.12.0 and deny warnings

.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

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

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

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.