Commit 680ab4e9 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents be9f621b 8b158ce9
......@@ -57,10 +57,8 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
Global Instance map_timeless `{! a : A, Timeless a} (g : gmap K A) : Timeless g.
Proof.
intros m Hm i. apply timeless; eauto with typeclass_instances.
Qed.
Global Instance map_timeless `{ a : A, Timeless a} (m : gmap K A) : Timeless m.
Proof. by intros m' ? i; apply (timeless _). Qed.
Instance map_empty_timeless : Timeless ( : gmap K A).
Proof.
......
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