diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 8e2a8cd0db8b310de86cc1c51131efb2fb9451ad..2283f79f3c8a7d4378abe4c47aa030d50aa46db7 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -37,7 +37,7 @@ Section definitions.
   Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
     (map_of_list pvs : gmap P V) !! p.
 
-  Definition first_resolve_in_list (R : proph_map P V) pvs :=
+  Definition first_resolve_in_list (R : proph_map P V) (pvs : proph_val_list P V) :=
     ∀ p v, p ∈ dom (gset _) R →
            first_resolve pvs p = Some v →
            R !! p = Some (Some v).
@@ -56,7 +56,6 @@ Section definitions.
   Definition proph := proph_aux.(unseal).
   Definition proph_eq :
     @proph = @proph_def := proph_aux.(seal_eq).
-
 End definitions.
 
 Section first_resolve.