From bba7474ed108f999f744a145a88ea9614c9f5841 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Oct 2018 08:07:51 +0200
Subject: [PATCH] Add type annotation.

---
 theories/heap_lang/proph_map.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 2283f79f3..21d9858d3 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) :=
-- 
GitLab