diff --git a/_CoqProject b/_CoqProject
index 54eb66339c6873fd8f95976deb3f8238c3f30d28..5aa77d4016e7cfbb8c81c57f5289d50130504ff5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,5 @@
 -Q theories actris
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
 theories/utils/auth_excl.v
 theories/utils/llist.v
 theories/utils/compare.v
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index b92b47cc79cfe8417c54c1ee3a9ba57917828205..ffb89b78aa4fdb5b636781f86d781932b88c1b21 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,9 +1,9 @@
 (** This file contains an instantiation of the
 Dependent Separation Protocols and an integration with the channel encodings.
 For starters this means fixing the types of messages to the
-value type of the language [val] and the logic to the iris logic [iProp Σ].
+value type of the language [val] and the logic to the Iris logic [iProp Σ].
 
-In doing so we define way of constructing instances of the instantiated type
+In doing so we define ways of constructing instances of the instantiated type
 via two constructors:
 - [iProto_end] which is identical to [proto_end]
 - [iProto_message] which takes an action and a continuation to construct
@@ -17,8 +17,8 @@ iProto_message with an appropriate continuation.
 
 Said continuation ultimately establishes the following:
 - Existential quantification of variables [x .. y].
-- The equivalence [v = w], where [w] is the value that is eventually sent.
-- Ownership of the predicate P
+- The equivalence [v = w], where [w] is the value that is eventually exchanged.
+- Ownership of the predicate [P]
 - A continuation as [prot]
 
 Futhermore type-specific variants of dual and append are provided:
@@ -29,9 +29,9 @@ An encoding of branching behaviour is additionally included, defined
 in terms of sending and receiving boolean flags:
 - [prot1 {Q1}<+>{Q2} prot2] and
 - [prot1 {Q1}<&>{Q2} prot2] which defines ownership of Q1 or Q2, and continues as
-Q1 or Q2, based on the sent or received flag.
+Q1 or Q2, based on the exchanged flag.
 
-The logical connective of protocol ownership are then defined:
+The logical connective of protocol ownership is then defined:
 - [c ↣  prot] which describes that channel endpoint [c] adheres
 to protocol [prot], achieved through Iris invariants and ghost state along
 with the logical connectives of the channel encodings [is_chan] and [chan_own]. 
@@ -88,7 +88,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq : @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
 Arguments iProto_message {_ _} _ _%proto.
-Instance: Params (@iProto_message) 3.
+Instance: Params (@iProto_message) 3 := {}.
 
 Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
   (iProto_message
@@ -167,11 +167,11 @@ Notation "'END'" := iProto_end : proto_scope.
 Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
   proto_map action_dual cid cid p.
 Arguments iProto_dual {_} _%proto.
-Instance: Params (@iProto_dual) 1.
+Instance: Params (@iProto_dual) 1 := {}.
 Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
   if d then iProto_dual p else p.
 Arguments iProto_dual_if {_} _ _%proto.
-Instance: Params (@iProto_dual_if) 2.
+Instance: Params (@iProto_dual_if) 2 := {}.
 
 (** Branching *)
 Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
@@ -179,7 +179,7 @@ Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
   (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
 Typeclasses Opaque iProto_branch.
 Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
-Instance: Params (@iProto_branch) 2.
+Instance: Params (@iProto_branch) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
 Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
 Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
@@ -192,7 +192,7 @@ Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
 (** Append *)
 Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
 Arguments iProto_app {_} _%proto _%proto.
-Instance: Params (@iProto_app) 1.
+Instance: Params (@iProto_app) 1 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 
 (** Auxiliary definitions and invariants *)
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index a04a43f210e10d904a30d682a7a67f4407b59735..172a45122b550eae0490879660af32134e73f902 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -4,7 +4,7 @@ and map and the necessary typeclass instances.
 
 They are designed with inspiration from Session Types, mimicking
 their constructors !T.st, ?T.st and END, respectively representing
-sending and receiving messages of type T or termination.
+sending and receiving messages of type T and termination.
 The main difference is that the protocols are defined over predicates,
 in place of types.
 
@@ -22,20 +22,19 @@ The remainder (V → (▶ [proto] → PROP) → PROP)) is a continuation that
 depends on the communicated value V and the dependent tail (▶ proto → PROP)
 from protocols guarded under laters to the propositions of the logic.
 
-The constructors of the protocol are then:
+The constructors of the protocol are:
 - [proto_end] which constructs the left-side of the sum.
 - [proto_msg] which takes an action and a continuation and constructs the
 right-hand side of the sum accodingly.
 
 The type is defined as a solution to a recursive domain
-equation, as it is self-referential under the guard of â–¶.
+equation, as it is self-referential under the guard of [â–¶ ].
 
 The available functions on [proto] are:
-- [proto_map] which can be used to map the actions, the propositions of
+- [proto_map] which can be used to map the actions and the propositions of
 a given protocol.
 - [proto_app] which appends two protocols [p1] and [p2], by substituting
- all terminations in [p1] with [p2].
-*)
+ all terminations in [p1] with [p2].*)
 
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
@@ -149,7 +148,7 @@ Definition proto_app_flipped {V} `{!Cofe PROPn, !Cofe PROP}
   fixpoint (proto_app_flipped_aux p2).
 Definition proto_app {V} `{!Cofe PROPn, !Cofe PROP}
   (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP := proto_app_flipped p2 p1.
-Instance: Params (@proto_app) 5.
+Instance: Params (@proto_app) 5 := {}.
 
 Lemma proto_app_flipped_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
   proto_app_flipped p2 p1 ≡ proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index a14aa347e8d95aaa2df2c94735cab7f814e5d3ec..b69df0464b70f8a679c96aca4756c5db0d322f3d 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -10,7 +10,7 @@ From iris.algebra Require Import gmultiset.
 Definition map_reduce {A B C} `{EqDecision K}
     (map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
   mbind (curry red) ∘ group ∘ mbind map.
-Instance: Params (@map_reduce) 7.
+Instance: Params (@map_reduce) 7 := {}.
 
 (** Distributed version *)
 Definition par_map_reduce_map : val :=
diff --git a/theories/utils/auth_excl.v b/theories/utils/auth_excl.v
index c9e35187c39a970f26ce3cf089e8f6cc84c69c34..5c7691f7583f8f735627cf0ff59744e16b09e0f1 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -24,7 +24,7 @@ Proof. solve_inG. Qed.
 
 Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
   Excl' a.
-Instance: Params (@to_auth_excl) 1.
+Instance: Params (@to_auth_excl) 1 := {}.
 
 Section auth_excl_ofe.
   Context {A : ofeT}.
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 8202458d6095cb5c1d0511dd0e3320a6e44a6c3a..496150ec7b1ebb0eb7fd88dda8548475ff916a07 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -27,12 +27,12 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp 
    then x ≡ ε ∗ own γ (● (Some (Cinr (Excl ())))) ∗ own γ (◯ (Some (Cinr (Excl ()))))
    else own γ (● (Some (Cinl (Pos.of_nat n, x)))))%I.
 Typeclasses Opaque server.
-Instance: Params (@server) 6.
+Instance: Params (@server) 6 := {}.
 
 Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
   own γ (◯ (Some (Cinl (1%positive, x)))).
 Typeclasses Opaque client.
-Instance: Params (@client) 5.
+Instance: Params (@client) 5 := {}.
 
 Section contribution.
   Context `{contributionG Σ A}.
diff --git a/theories/utils/group.v b/theories/utils/group.v
index 9b3b0b0a715fd424e782a339db46db78ad3acf75..15490997feae760dbeecfc5e6e84a2450690a7b4 100644
--- a/theories/utils/group.v
+++ b/theories/utils/group.v
@@ -17,8 +17,8 @@ Fixpoint group {A} `{EqDecision K} (ixs : list (K * A)) : list (K * list A) :=
   | (i,x) :: ixs => group_insert i x (group ixs)
   end.
 
-Instance: Params (@group_insert) 5.
-Instance: Params (@group) 3.
+Instance: Params (@group_insert) 5 := {}.
+Instance: Params (@group) 3 := {}.
 
 Local Infix "≡ₚₚ" :=
   (PermutationA (prod_relation (=) (≡ₚ))) (at level 70, no associativity) : stdpp_scope.