diff --git a/theories/logic/model.v b/theories/logic/model.v
index a5b808d2303c1720c5dbd6ccba566861654e453c..1b4e4b566d1afde5e8a8d4e53cc10df3ac2e5151 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -17,6 +17,7 @@ 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.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index b816af339aaeb9d6c58d3456be62845c1d8aecbc..83bb2b65b968ef1031cc7fb89f9142d42b51d334 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -61,6 +61,7 @@ Definition unop_bool_res_type (op : un_op) : option type :=
   | _ => None
   end.
 
+Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
 Notation "()" := TUnit : FType_scope.