From 5ec0e1f59873c3fff5b2e3fe4661db9a5ab65daa Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Fri, 31 May 2019 17:26:18 +0200
Subject: [PATCH] Some [positive] was sometimes used for [loc], which is now
 abstract.

---
 opam                           | 2 +-
 theories/spanning_tree/mon.v   | 4 ++--
 theories/spanning_tree/proof.v | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/opam b/opam
index a12fbc41..9931da43 100644
--- a/opam
+++ b/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" }
 ]
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index aaaaee2a..9e14e57a 100644
--- a/theories/spanning_tree/mon.v
+++ b/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)).
diff --git a/theories/spanning_tree/proof.v b/theories/spanning_tree/proof.v
index 363d5676..ef7282fd 100644
--- a/theories/spanning_tree/proof.v
+++ b/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. }
-- 
GitLab