From e028d36b87d46885267b6f1c9ab9567207c82a6e Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Thu, 3 Oct 2024 09:38:10 +0200
Subject: [PATCH] bump to Coq 8.19.2 and Iris

---
 README.md                |  2 +-
 coq-gpfsl.opam           |  2 +-
 coq-orc11.opam           |  2 +-
 gpfsl/base_logic/vprop.v |  4 ++--
 gpfsl/lang/lang.v        | 28 ++++++++++++++--------------
 5 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/README.md b/README.md
index 65c80324..23da1269 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is a separation logic for ORC11 based on [iGPS] and [FSL]. It has been rece
 
 This version is known to compile with:
 
- - Coq 8.18.0
+ - Coq 8.19.2
  - A development version of [Iris].
 
 The easiest way to install the correct versions of the dependencies is through
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 8bd60d0c..078bc054 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2024-09-10.0.f14ebfde") | (= "dev") }
+  "coq-iris"  { (= "dev.2024-10-02.2.636308c8") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index afe5394e..8e4ad170 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2024-09-08.0.d37b5e70") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-10-02.0.2dd41ab5") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl/base_logic/vprop.v b/gpfsl/base_logic/vprop.v
index 5cf50216..69c536a9 100644
--- a/gpfsl/base_logic/vprop.v
+++ b/gpfsl/base_logic/vprop.v
@@ -46,8 +46,8 @@ Definition view_at_eq : @view_at = _ := seal_eq _.
 
 End defs.
 
-Arguments view_join {_} _ _%I : simpl never.
-Arguments view_at {_} _ _%I : simpl never.
+Arguments view_join {_} _ _%_I : simpl never.
+Arguments view_at {_} _ _%_I : simpl never.
 
 Notation "'⊔{' V '}' P" := (view_join V P) (at level 25, format "⊔{ V }  P") : bi_scope.
 Notation "'@{' V '}' P" := (view_at V P) (at level 25, format "@{ V }  P") : bi_scope.
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index c7125e81..c3f5f361 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -61,17 +61,17 @@ Module base.
   Bind Scope expr_scope with expr.
   Delimit Scope expr_scope with E.
 
-  Arguments Rec _ _ _%E.
-  Arguments App _%E _%E.
-  Arguments UnOp _ _%E.
-  Arguments BinOp _ _%E _%E.
-  Arguments Case _%E _%E.
-  Arguments Fork _%E.
-  Arguments Read _ _%E.
-  Arguments Write _ _%E _%E.
-  Arguments CAS _%E _%E _%E _ _.
-  Arguments Alloc _%E.
-  Arguments Free _%E _%E.
+  #[global] Arguments Rec _ _ _%_E.
+  #[global] Arguments App _%_E _%_E.
+  #[global] Arguments UnOp _ _%_E.
+  #[global] Arguments BinOp _ _%_E _%_E.
+  #[global] Arguments Case _%_E _%_E.
+  #[global] Arguments Fork _%_E.
+  #[global] Arguments Read _ _%_E.
+  #[global] Arguments Write _ _%_E _%_E.
+  #[global] Arguments CAS _%_E _%_E _%_E _ _.
+  #[global] Arguments Alloc _%_E.
+  #[global] Arguments Free _%_E _%_E.
 
   Fixpoint is_closed (X : list string) (e : expr) : bool :=
     match e with
@@ -182,12 +182,12 @@ Module base.
     | _, _ => None
     end.
 
-  Arguments subst_l _%binder _ _%E.
+  Arguments subst_l _%_binder _ _%_E.
 
   Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                      (e : expr) : expr :=
     Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
-  Arguments subst_v _%binder _ _%E.
+  Arguments subst_v _%_binder _ _%_E.
 
   Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
     Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
@@ -760,7 +760,7 @@ Module nopro_lang.
           lbl_machine_step 𝓥 σ.(mem) σ.(sc) evt2 ot2 𝑚s2 𝓥2 M2 𝓢2 →
           drf_pre σ.(na) 𝓥 σ.(mem) evt2)
     : base_step (mkExpr e 𝓥) σ [] (mkExpr e' 𝓥') (mkGB 𝓢' 𝓝' M') efs.
-  Arguments base_step _%E _ _ _%E _ _%E.
+  Arguments base_step _%_E _ _ _%_E _ _%_E.
 
   Lemma base_step_tview_sqsubseteq e 𝓥 σ κs e' 𝓥' σ' ef
     (STEP: base_step (mkExpr e 𝓥) σ κs (mkExpr e' 𝓥') σ' ef) :
-- 
GitLab