Commit 5ec0e1f5 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre

Some [positive] was sometimes used for [loc], which is now abstract.

parent 3e2bbf56
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-05-30.1.78ee4940") | (= "dev") }
"coq-iris" { (= "dev.2019-05-31.0.5c07c3be") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -751,7 +751,7 @@ Proof.
by rewrite get_left_singleton get_right_singleton /get_left /get_right Hu.
Qed.
Lemma mark_strict_subgraph (g : graph loc) (G : Gmon) x v :
((x [] v) G) x dom (gset positive) g
((x [] v) G) x dom (gset loc) g
of_graph g G !! x = Some (false, v) strict_subgraph g (Gmon_graph G)
strict_subgraph g (Gmon_graph ((x [] v) G)).
Proof.
......@@ -760,7 +760,7 @@ Proof.
inversion 1; auto using strict_sub_children_refl.
Qed.
Lemma update_strict_subgraph (g : graph loc) (G : Gmon) x v w :
((x [] v) G) x dom (gset positive) g
((x [] v) G) x dom (gset loc) g
strict_subgraph g (Gmon_graph ((x [] w) G))
strict_sub_children w v
strict_subgraph g (Gmon_graph ((x [] v) G)).
......
......@@ -51,7 +51,7 @@ Section wp_span.
[by iFrame|].
iDestruct (own_graph_valid with "Hl1") as %Hvl.
iExists (Gmon_graph G').
assert (dom (gset positive) g = dom (gset positive) (Gmon_graph G')).
assert (dom (gset loc) g = dom (gset loc) (Gmon_graph G')).
{ erewrite front_t_t_dom; eauto.
- by rewrite Gmon_graph_dom.
- eapply front_mono; rewrite Gmon_graph_dom; eauto. }
......
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