From 8b158ce96342cd98b8ed3ec60dcd1ae4ecf9b414 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Feb 2016 20:09:07 +0100
Subject: [PATCH] Use correct variable names for map_timeless.

---
 algebra/fin_maps.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 531010863..9b4817ff0 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -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.
-- 
GitLab