From 03a0069deefe17688797b095455523bf7de50661 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Thu, 3 Oct 2024 10:27:32 +0200
Subject: [PATCH] Bump to Coq 8.19.1 and new gpfsl

---
 .gitlab-ci.yml             |  4 ++--
 README.md                  |  4 ++--
 coq-lambda-rust.opam       |  2 +-
 theories/typing/programs.v | 12 ++++++------
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e2cd966c..fac254d6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.18.0:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.19.1"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
   tags:
diff --git a/README.md b/README.md
index 8d124b29..b102f027 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying RBrlx.
 
 This version is known to compile with:
 
- - Coq 8.18.0
+ - Coq 8.19.1
  - A development version of [GPFSL].
 
 ## Building from source
@@ -216,4 +216,4 @@ The verification of Full Arc is split into 2 parts:
   mismatches.
 
   [GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/
-  [ORC11]: https://gitlab.mpi-sws.org/iris/orc11/
+  [ORC11]: https://gitlab.mpi-sws.org/iris/gpfsl/-/tree/master/orc11
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index c325151b..a19b2738 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2024-09-10.1.5365229f") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-10-03.0.023610f8") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d5c811cf..dfe10bc6 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -15,7 +15,7 @@ Section typing.
     (∀ tid (qmax : Qp), ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
                cctx_interp tid qmax C -∗ tctx_interp tid T -∗
                WP e @ tid; ⊤ {{ _, cont_postcondition }})%I.
-  Global Arguments typed_body _ _ _ _ _%E.
+  Global Arguments typed_body _ _ _ _ _%_E.
 
   Global Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
@@ -64,7 +64,7 @@ Section typing.
               llctx_interp qmax L -∗ tctx_interp tid T1 -∗
        WP e @ tid; ⊤ {{ v, na_own tid ⊤ ∗
                          llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
-  Global Arguments typed_instruction _ _ _ _%E _.
+  Global Arguments typed_instruction _ _ _ _%_E _.
 
   (** Writing and Reading **)
   Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
@@ -76,7 +76,7 @@ Section typing.
   Definition typed_write_aux : seal (@typed_write_def). Proof. by eexists. Qed.
   Definition typed_write := typed_write_aux.(unseal).
   Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
-  Global Arguments typed_write _ _ _%T _%T _%T.
+  Global Arguments typed_write _ _ _%_T _%_T _%_T.
 
   Global Instance typed_write_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_write E L ty1 ty ty2).
@@ -97,7 +97,7 @@ Section typing.
   Definition typed_read_aux : seal (@typed_read_def). Proof. by eexists. Qed.
   Definition typed_read := typed_read_aux.(unseal).
   Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
-  Global Arguments typed_read _ _ _%T _%T _%T.
+  Global Arguments typed_read _ _ _%_T _%_T _%_T.
 
   Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_read E L ty1 ty ty2).
@@ -107,11 +107,11 @@ End typing.
 Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : vPropI Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
-Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+Arguments typed_instruction_ty {_ _} _ _ _ _%_E _%_T.
 
 Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
-Arguments typed_val _ _ _%V _%T.
+Arguments typed_val _ _ _%_V _%_T.
 
 Section typing_rules.
   Context `{!typeG Σ}.
-- 
GitLab