diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 391ba81a25e1e6ed34aaa90b7f64e78fb0dc3043..1a6325ed232f407d6c74e1ce6d67231f07af18c3 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -117,7 +117,7 @@ Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
-Typeclasses Opaque iProto_choice.
+Global Typeclasses Opaque iProto_choice.
 Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
 Global Instance: Params (@iProto_choice) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index e24fb86b24e9f3d65c5c0f60449a05bbe8af2002..ff04b1700a0231b6c3f1d26ae7a64d9d5bcc8e87 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1289,7 +1289,7 @@ Section proto.
 
 End proto.
 
-Typeclasses Opaque iProto_ctx iProto_own.
+Global Typeclasses Opaque iProto_ctx iProto_own.
 
 Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index ce5be825714f843d334543934ec1be3aba8de8da..9075dffb824090aac90491182ca1c3f4462b3d7a 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -16,7 +16,7 @@ Definition ltyped `{!heapGS Σ}
     (Γ1 Γ2 : ctx Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
   tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗
     WP subst_map vs e {{ v, ltty_car A v ∗ ctx_ltyped vs Γ2 }})%I.
-Instance: Params (@ltyped) 2 := {}.
+Global Instance: Params (@ltyped) 2 := {}.
 
 Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
   (at level 100, e at next level, A at level 200) : bi_scope.
@@ -57,7 +57,7 @@ The value typing judgement subsumes the typing judgement on expressions,
 as made precise by the [ltyped_val_ltyped] lemma. *)
 Definition ltyped_val `{!heapGS Σ} (v : val) (A : ltty Σ) : iProp Σ :=
   tc_opaque (â–  ltty_car A v)%I.
-Instance: Params (@ltyped_val) 3 := {}.
+Global Instance: Params (@ltyped_val) 3 := {}.
 Notation "⊨ᵥ v : A" := (ltyped_val v A)
   (at level 100, v at next level, A at level 200) : bi_scope.
 Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 6435034c4797d128f89bca05d7a531f70f80d34c..cb78e4f3bf661a067927433ff5294fddac1cdc39 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -29,12 +29,12 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp 
   (if decide (n = O)
    then x ≡ ε ∗ own γ (● (Some (Cinr (Excl ())))) ∗ own γ (◯ (Some (Cinr (Excl ()))))
    else own γ (● (Some (Cinl (Pos.of_nat n, x)))))%I.
-Typeclasses Opaque server.
+Global Typeclasses Opaque server.
 Global Instance: Params (@server) 6 := {}.
 
 Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
   own γ (◯ (Some (Cinl (1%positive, x)))).
-Typeclasses Opaque client.
+Global Typeclasses Opaque client.
 Global Instance: Params (@client) 5 := {}.
 
 Section contribution.