Remove old FIXME.

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