diff --git a/theories/gmap.v b/theories/gmap.v
index ed33a9d38da038b123ed3ee4382bf2c14987ac3f..f8ab424c85df15cf78e216f84381518d85c2d4d3 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. }