From ec5b6bd845da038c500516ad6a28a84db98534ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Feb 2021 22:03:43 +0100
Subject: [PATCH] Remove old FIXME.

---
 theories/gmap.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/gmap.v b/theories/gmap.v
index f8ab424c..ed33a9d3 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -157,10 +157,8 @@ 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 : option (gmap K2 A)) ≫= (.!! j).
+    gmap_curry m !! (i,j) = m !! i ≫= (.!! j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
     { by rewrite !lookup_empty. }
@@ -177,7 +175,7 @@ Section curry_uncurry.
   Qed.
 
   Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
-    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
+    gmap_uncurry m !! i ≫= (.!! j) = m !! (i, j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
     { by rewrite !lookup_empty. }
-- 
GitLab