Commit f1f34470 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add missing type in a signature.

parent f238c358
...@@ -37,7 +37,7 @@ Section definitions. ...@@ -37,7 +37,7 @@ Section definitions.
Definition first_resolve (pvs : proph_val_list P V) (p : P) := Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
(map_of_list pvs : gmap P V) !! 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 p v, p dom (gset _) R
first_resolve pvs p = Some v first_resolve pvs p = Some v
R !! p = Some (Some v). R !! p = Some (Some v).
...@@ -56,7 +56,6 @@ Section definitions. ...@@ -56,7 +56,6 @@ Section definitions.
Definition proph := proph_aux.(unseal). Definition proph := proph_aux.(unseal).
Definition proph_eq : Definition proph_eq :
@proph = @proph_def := proph_aux.(seal_eq). @proph = @proph_def := proph_aux.(seal_eq).
End definitions. End definitions.
Section first_resolve. Section first_resolve.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment