From b36ebb939b5fdded3024ed5d4d10b93efee4e8c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Sep 2020 14:02:07 +0200
Subject: [PATCH] Fix warnings.

---
 theories/logic/model.v  | 1 +
 theories/typing/types.v | 1 +
 2 files changed, 2 insertions(+)

diff --git a/theories/logic/model.v b/theories/logic/model.v
index a5b808d..1b4e4b5 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 b816af3..83bb2b6 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.
-- 
GitLab