diff --git a/theories/channel/proto.v b/theories/channel/proto.v index 13b3a4620e34c24f4b195536fc4b8d7898e09946..92c4c0041d3c88e7b542315014ac3a0f209ab8c9 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.