From 81022281c6d489f3858921fe83c1333b7c9081ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 May 2017 11:53:08 +0200
Subject: [PATCH] Compatibility with Coq 8.5.

---
 theories/fin_maps.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0c8c8efa..2cc3150a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -261,7 +261,7 @@ Lemma map_subset_alt {A} (m1 m2 : M A) :
 Proof.
   rewrite strict_spec_alt. split.
   - intros [? Heq]; split; [done|].
-    destruct (decide (Exists (λ '(i,_), m1 !! i = None) (map_to_list m2)))
+    destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
       as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
          |Hm%(not_Exists_Forall _)]; [eauto|].
     destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi].
-- 
GitLab