Commit 8b158ce9 authored by Robbert Krebbers's avatar Robbert Krebbers

Use correct variable names for map_timeless.

parent 1c8ba455
......@@ -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