Skip to content
Snippets Groups Projects
Commit 69e9e8d2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add all instance arguments, needed for compilation with recent Coq.

parent d7f2e1a0
No related branches found
No related tags found
No related merge requests found
......@@ -83,7 +83,7 @@ Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
Section session_types.
Context {Σ : gFunctors}.
Global Instance lty_msg_exist_ne k :
Global Instance lty_msg_exist_ne k n :
Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
Proof. solve_proper. Qed.
Global Instance lty_msg_exist_proper k :
......@@ -107,11 +107,11 @@ Section session_types.
Proof. solve_proper. Qed.
Global Instance lty_choice_proper a : Proper (() ==> ()) (@lty_choice Σ a).
Proof. apply ne_proper, _. Qed.
Global Instance lty_choice_contractive a :
Global Instance lty_choice_contractive a n :
Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
(@lty_choice Σ a).
Proof.
intros n Ss Ts Heq. rewrite /lty_choice.
intros Ss Ts Heq. rewrite /lty_choice.
do 2 f_equiv. f_equiv => i.
rewrite !lookup_total_alt.
specialize (Heq i).
......
......@@ -34,7 +34,7 @@ Section subtyping.
Global Instance lty_bi_le_plain {k} (M1 M2 : lty Σ k) : Plain (M1 <:> M2).
Proof. rewrite /lty_bi_le /=. apply _. Qed.
Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
Global Instance lty_le_ne k : NonExpansive2 (@lty_le Σ k).
Proof. destruct k; solve_proper. Qed.
Global Instance lty_le_proper {k} : Proper (() ==> () ==> ()) (@lty_le Σ k).
Proof. apply (ne_proper_2 _). Qed.
......
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