From f1f344702b2ef87bed350efe62f9f7fbd02b17ab Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 21 Oct 2018 11:01:18 +0200
Subject: [PATCH] Add missing type in a signature.

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

diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 8e2a8cd0d..2283f79f3 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.
-- 
GitLab