From 336a6e9dab6d70ef55b7f07705ca7fe48ecbb565 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Thu, 12 May 2022 13:10:52 +0200
Subject: [PATCH] Added global flags to fix typeclass warnings

---
 theories/channel/channel.v             | 2 +-
 theories/channel/proto.v               | 2 +-
 theories/logrel/term_typing_judgment.v | 4 ++--
 theories/utils/contribution.v          | 4 ++--
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 391ba81..1a6325e 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 e24fb86..ff04b17 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 ce5be82..9075dff 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 6435034..cb78e4f 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.
-- 
GitLab