Merge branch 'fix' into 'master'

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

See merge request !18

opam

@@ -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" }
 ]

theories/spanning_tree/mon.v

@@ -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)).

theories/spanning_tree/proof.v

@@ -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. }