Skip to content
Snippets Groups Projects
Commit 336a6e9d authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added global flags to fix typeclass warnings

parent 09b48e91
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
......@@ -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.
......@@ -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)
......
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment