From 9fbc1013c78f96a22afc1c0d6e2ce499b195d54f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Mar 2019 12:58:18 +0100
Subject: [PATCH] No longer break `gset` abstraction.
---
theories/spanning_tree/mon.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index 4dfce4ea..0ef578b5 100644
--- a/theories/spanning_tree/mon.v
+++ b/theories/spanning_tree/mon.v
@@ -80,7 +80,7 @@ Definition Gmon_graph (G : Gmon) : graph loc := omap excl_chlC_chl G.
Definition Gmon_graph_dom (G : Gmon) :
✓ G → dom (gset loc) (Gmon_graph G) = dom (gset _) G.
Proof.
- intros Hvl; apply mapset_eq => i. rewrite ?elem_of_dom lookup_omap.
+ intros Hvl; apply elem_of_equiv_L=> i. rewrite !elem_of_dom lookup_omap.
specialize (Hvl i). split.
- revert Hvl; case _ : (G !! i) => [[]|] //=; eauto.
intros _ [? Hgi]; inversion Hgi.
@@ -230,7 +230,7 @@ Proof. intros H. by rewrite lookup_op lookup_singleton_ne //= left_id_L. Qed.
Lemma of_graph_dom g G : dom (gset loc) (of_graph g G) = dom (gset _) g.
Proof.
- apply mapset_eq=>i.
+ apply elem_of_equiv_L=>i.
rewrite ?elem_of_dom lookup_imap /of_graph_elem lookup_omap.
case _ : (g !! i) => [x|]; case _ : (G !! i) => [[]|] //=; split;
intros [? Hcn]; inversion Hcn; eauto.
--
GitLab