diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 2283f79f3c8a7d4378abe4c47aa030d50aa46db7..21d9858d3f72adfcdb3649fde23bf60a3864dfdd 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -34,7 +34,7 @@ Section definitions.
   Context `{pG : proph_mapG P V Σ}.
 
   (** The first resolve for [p] in [pvs] *)
-  Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
+  Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
     (map_of_list pvs : gmap P V) !! p.
 
   Definition first_resolve_in_list (R : proph_map P V) (pvs : proph_val_list P V) :=