From 7e6a682ed9ccf90ea760f57e7e6022ffbb13f8e5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Feb 2021 22:23:48 +0100
Subject: [PATCH] Revert "Remove old FIXME."
This reverts commit ec5b6bd845da038c500516ad6a28a84db98534ee.
The FIXME seems to not just rely on https://github.com/coq/coq/issues/5735
since it fails with Coq 8.10 and 8.11
---
theories/gmap.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/gmap.v b/theories/gmap.v
index ed33a9d3..f8ab424c 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -157,8 +157,10 @@ Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
Section curry_uncurry.
Context `{Countable K1, Countable K2} {A : Type}.
+ (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
+ a consequence of Coq bug #5735 *)
Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
- gmap_curry m !! (i,j) = m !! i ≫= (.!! j).
+ gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (.!! j).
Proof.
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
{ by rewrite !lookup_empty. }
@@ -175,7 +177,7 @@ Section curry_uncurry.
Qed.
Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
- gmap_uncurry m !! i ≫= (.!! j) = m !! (i, j).
+ (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
Proof.
apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
{ by rewrite !lookup_empty. }
--
GitLab