Commit 8004a1a6 authored by Ralf Jung's avatar Ralf Jung

fix Coq 8.9 deprecation warnings

parent 9a3bc1ef
......@@ -21,7 +21,7 @@ Notation map := (cFunctor_map F).
Fixpoint A (k : nat) : ofeT :=
match k with 0 => unitC | S k => F (A k) end.
Local Instance: k, Cofe (A k).
Proof using Fcofe. induction 0; apply _. Defined.
Proof using Fcofe. induction k; apply _. Defined.
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
......
......@@ -64,7 +64,7 @@ Qed.
Global Instance frame_step_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /collection_equiv_spec [??]; split; by apply frame_step_mono. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Global Instance up_preserving : Proper ((=) ==> flip () ==> ()) up.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment