From f5bf3f84b6ba801741a386f9e1d68a7c8f0ea76d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Oct 2024 10:58:31 +0100
Subject: [PATCH] Fix warnings.

---
 .gitlab-ci.yml                  |  1 +
 _CoqProject                     |  2 --
 coq-actris.opam                 |  2 +-
 theories/channel/channel.v      |  4 ++--
 theories/channel/proofmode.v    |  4 ++--
 theories/channel/proto.v        | 18 +++++++++---------
 theories/logrel/model.v         |  4 ++--
 theories/logrel/session_types.v |  2 +-
 8 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3a39912..33ac6a4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -32,6 +32,7 @@ build-coq.8.20.0:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.20.0"
+    DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   tags:
   - fp-timing
diff --git a/_CoqProject b/_CoqProject
index d356d99..858ff55 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,8 +4,6 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# Fixing this one requires Coq 8.19
--arg -w -arg -argument-scope-delimiter
 
 theories/utils/llist.v
 theories/utils/compare.v
diff --git a/coq-actris.opam b/coq-actris.opam
index 940fffa..70cd101 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-10-03.0.4871f965") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-10-07.0.6dece417") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 1212dfb..d6f23c5 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -98,7 +98,7 @@ Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
 Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
 Definition iProto_pointsto_eq :
   @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
-Arguments iProto_pointsto {_ _ _} _ _%proto.
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
 Global Instance: Params (@iProto_pointsto) 4 := {}.
 Notation "c ↣ p" := (iProto_pointsto c p)
   (at level 20, format "c  ↣  p").
@@ -111,7 +111,7 @@ Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
 Global Typeclasses Opaque iProto_choice.
-Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
+Arguments iProto_choice {_} _ _%_I _%_I _%_proto _%_proto.
 Global Instance: Params (@iProto_choice) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
 Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8264464..c8e5f41 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -36,7 +36,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
 Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
-Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
@@ -46,7 +46,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
 Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
-Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
 
 Section classes.
   Context `{!chanG Σ, !heapGS Σ}.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index e915722..531c871 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -108,7 +108,7 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%V _%I _%proto.
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
 Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
@@ -117,12 +117,12 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%msg.
+Arguments iMsg_exist {_ _ _} _%_msg.
 Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%msg /.
+Arguments iMsg_texist {_ _ !_} _%_msg /.
 
 Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
   (at level 200, v at level 20, right associativity,
@@ -157,7 +157,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%msg.
+Arguments iProto_message {_ _} _ _%_msg.
 Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
@@ -225,7 +225,7 @@ Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
 Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%proto _%proto.
+Arguments iProto_app {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
@@ -236,13 +236,13 @@ Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%proto.
+Arguments iProto_dual {_ _} _%_proto.
 Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%proto.
+Arguments iProto_dual_if {_ _} _ _%_proto.
 Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Protocol entailment *)
@@ -277,7 +277,7 @@ Proof.
 Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
+Arguments iProto_le {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
@@ -316,7 +316,7 @@ Definition iProto_ctx `{protoG Σ V}
 (** * The connective for ownership of channel ends *)
 Definition iProto_own `{!protoG Σ V} (γ : gname) (p : iProto Σ V) : iProp Σ :=
   ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ p'.
-Arguments iProto_own {_ _ _} _ _%proto.
+Arguments iProto_own {_ _ _} _ _%_proto.
 Global Instance: Params (@iProto_own) 4 := {}.
 
 Global Instance iProto_own_contractive `{protoG Σ V} γ :
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index dad8455..10a4359 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -24,8 +24,8 @@ Global Instance kind_inhabited : Inhabited kind := populate tty_kind.
 Variant lty Σ : kind → Type :=
   | Ltty : (val → iProp Σ) → lty Σ tty_kind
   | Lsty : iProto Σ → lty Σ sty_kind.
-Arguments Ltty {_} _%I.
-Arguments Lsty {_} _%proto.
+Arguments Ltty {_} _%_I.
+Arguments Lsty {_} _%_proto.
 
 Declare Scope lty_scope.
 Bind Scope lty_scope with lty.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 4d0c7ea..d1a27ef 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -19,7 +19,7 @@ Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
 
 Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) : lmsg Σ :=
   ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
-Arguments lty_msg_texist {_ !_} _%lmsg /.
+Arguments lty_msg_texist {_ !_} _%_lmsg /.
 
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
-- 
GitLab