From f238c358147ada6508a645a37f701ace1ed1ad8c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 19 Oct 2018 09:26:02 +0200
Subject: [PATCH] fix compatibility with Coq 8.7
---
theories/heap_lang/proph_map.v | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 5f19f0c77..8e2a8cd0d 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -72,9 +72,10 @@ Section first_resolve.
first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
Proof.
intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
- erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
- - by rewrite lookup_insert.
- - rewrite lookup_insert_ne; first auto. by intros ->.
+ erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin].
+ - intros ->. by rewrite lookup_insert.
+ - intros <-%Hf; last done. rewrite lookup_insert_ne; first done.
+ intros ?. subst. done.
Qed.
Lemma first_resolve_delete pvs p v R :
--
GitLab