diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index ef7dd6f3f5fef929891bcdb2e4c4b21a9419f741..7eef5ceb2f7e3fe42edd6df819a4b35c0866b717 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -67,6 +67,7 @@ Proof. solve_inG. Qed.
 
 (** * Types *)
 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.
@@ -79,6 +80,7 @@ End iMsg.
 Arguments IMsg {_ _} _.
 Arguments iMsg_car {_ _} _.
 
+Declare Scope msg_scope.
 Delimit Scope msg_scope with msg.
 Bind Scope msg_scope with iMsg.
 Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 2ec4fab7191011449ad526fea46ccb86c7f27a82..3f4f580f242a845eca4e171d7ec3896546dcfffb 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -55,7 +55,7 @@ Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
 
 Definition proto_result (V : Type) := result_2 (proto_auxOF V).
 Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
-  proto_result V PROPn _ PROP _.
+  solution_2_car (proto_result V) PROPn _ PROP _.
 Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
 Proof. apply _. Qed.
 Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index 3d558153c5ce1821f295a711faae70027426a8da..e7223327a4a3b4ea658ded35dda80dcfd6e9c274 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -20,13 +20,14 @@ Instance kind_eq_dec : EqDecision kind.
 Proof. solve_decision. Defined.
 Instance kind_inhabited : Inhabited kind := populate tty_kind.
 
-(** Use [Variant] to supress generation of induction schemes *)
+(** Use [Variant] to suppress generation of induction schemes *)
 Variant lty Σ : kind → Type :=
   | Ltty : (val → iProp Σ) → lty Σ tty_kind
   | Lsty : iProto Σ → lty Σ sty_kind.
 Arguments Ltty {_} _%I.
 Arguments Lsty {_} _%proto.
 
+Declare Scope lty_scope.
 Bind Scope lty_scope with lty.
 Delimit Scope lty_scope with lty.
 
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 3bea14a061bc9652fc0814c750db7160eb907bc8..435460caedeeaac345d4c97894e9f172f11215cd 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -7,6 +7,7 @@ From actris.logrel Require Export model telescopes.
 From actris.channel Require Export channel.
 
 Definition lmsg Σ := iMsg Σ.
+Declare Scope lmsg_scope.
 Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
diff --git a/theories/utils/cofe_solver_2.v b/theories/utils/cofe_solver_2.v
index 3b8c5e401e1844f938b06f20f267da58eb615d5d..ef243523de100308412f23deb971b22b24f5d658 100644
--- a/theories/utils/cofe_solver_2.v
+++ b/theories/utils/cofe_solver_2.v
@@ -3,11 +3,12 @@ From iris.algebra Require Import cofe_solver.
 (** Version of the cofe_solver for a parametrized functor. Generalize and move
 to Iris. *)
 Record solution_2 (F : ofeT → oFunctor) := Solution2 {
-  solution_2_car :> ∀ An `{!Cofe An} A `{!Cofe A}, ofeT;
+  solution_2_car : ∀ An `{!Cofe An} A `{!Cofe A}, ofeT;
   solution_2_cofe `{!Cofe An, !Cofe A} : Cofe (solution_2_car An A);
   solution_2_iso `{!Cofe An, !Cofe A} :>
     ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
 }.
+Arguments solution_2_car {F}.
 Existing Instance solution_2_cofe.
 
 Section cofe_solver_2.