Revert "Remove old FIXME."

This reverts commit ec5b6bd8.

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

@@ -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. }