No longer use `Declare Scope` since it does not work in Coq 8.9.

_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
+# "Declare Scope" does not exist yet in 8.9.
+-arg -w -arg -undeclared-scope
 # 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/logic/model.v

@@ -18,7 +18,6 @@ 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.

theories/typing/types.v

@@ -51,7 +51,6 @@ 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.