From 002cb8244f0d420b2517051e7b93a4d80b7e5f68 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Dec 2022 10:17:23 +0100
Subject: [PATCH] Type annotation in potential ambigious case.

---
 iris_heap_lang/metatheory.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index a45b2faa6..728d4debd 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -190,7 +190,7 @@ Qed.
 
 Lemma subst_map_empty e : subst_map ∅ e = e.
 Proof.
-  assert (∀ x, binder_delete x (∅:gmap _ val) = ∅) as Hdel.
+  assert (∀ x, binder_delete x (∅:gmap string val) = ∅) as Hdel.
   { intros [|x]; by rewrite /= ?delete_empty. }
   induction e; simplify_map_eq; rewrite ?Hdel; auto with f_equal.
 Qed.
-- 
GitLab