From 1422f908484404a86c77f7a84fea32ad2f7a97eb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Oct 2020 10:20:16 +0100
Subject: [PATCH] more old Coq failures

---
 theories/fin_map_dom.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 486ce529..eb51e26c 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -91,7 +91,10 @@ Proof.
 Qed.
 Lemma dom_insert_lookup {A} (m : M A) i x :
   is_Some (m !! i) → dom D (<[i:=x]>m) ≡ dom D m.
-Proof. intros Hindom%elem_of_dom. rewrite dom_insert. set_solver. Qed.
+Proof.
+  intros Hindom. assert (i ∈ dom D m) by by apply elem_of_dom.
+  rewrite dom_insert. set_solver.
+Qed.
 Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
 Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
-- 
GitLab