From ece0a511d0d314292070be5cb9a3f0c66d463f41 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Sun, 28 Jan 2024 22:15:33 +0100
Subject: [PATCH] Opened proto scope to avoid superfluous delimiters

---
 theories/channel/proto.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 13b3a46..92c4c00 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -70,7 +70,7 @@ Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
 Declare Scope proto_scope.
 Delimit Scope proto_scope with proto.
 Bind Scope proto_scope with iProto.
-Local Open Scope proto.
+Open Scope proto.
 
 (** * Messages *)
 Section iMsg.
-- 
GitLab