From 3a20cb6af532d44d6edd4d09ec3b14fef17ec021 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 16:49:41 +0100
Subject: [PATCH] fix compatibility with latest Coq 8.6
---
prelude/gmultiset.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v
index 52a77a7aa..c9e6d38bd 100644
--- a/prelude/gmultiset.v
+++ b/prelude/gmultiset.v
@@ -178,7 +178,7 @@ Proof.
destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements.
set (f xn := let '(x, n) := xn in replicate (S n) x); simpl.
revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
- { by rewrite (left_id_L _ _), map_to_list_empty. }
+ { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
destruct (Y !! x) as [n'|] eqn:HY.
- rewrite <-(insert_id Y x n'), <-(insert_delete Y) by done.
erewrite <-insert_union_with by done.
--
GitLab