Commit 63ed680f authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build on Coq 8.11

parent 28289a77
......@@ -131,7 +131,7 @@ Section lemmas.
Qed.
Lemma ghost_map_alloc_strong_empty P :
pred_infinite P
|==> γ, P γ⌝ ghost_map_auth γ 1 .
|==> γ, P γ⌝ ghost_map_auth γ 1 ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc_strong P ) as (γ) "(% & Hauth & _)"; eauto.
Qed.
......@@ -143,7 +143,7 @@ Section lemmas.
- eauto.
Qed.
Lemma ghost_map_alloc_empty :
|==> γ, ghost_map_auth γ 1 .
|==> γ, ghost_map_auth γ 1 ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc ) as (γ) "(Hauth & _)"; eauto.
Qed.
......
Supports Markdown
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