update dependencies

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-08-30.0.efb542b0") | (= "dev") }
+  "coq-iris"  { (= "dev.2024-09-04.0.0653ba6c") | (= "dev") }
   "coq-orc11" {= version}
 ]
 

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-08-30.1.8548ce42") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-09-03.0.6cb5c0f2") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]

gpfsl-examples/algebra/mono_list_list.v

@@ -5,8 +5,8 @@ From iris.prelude Require Import options.
 
 (* TODO: upstream? *)
 Lemma map_relation_iff `{∀ A, Lookup K A (M A)} {A B}
-    (R1 R2 : A → B → Prop) (P1 P2 : A → Prop) (Q1 Q2 : B → Prop)
-    (IffR : ∀ a b, R1 a b ↔ R2 a b) (IffP : ∀ a, P1 a ↔ P2 a) (IffQ : ∀ b, Q1 b ↔ Q2 b)
+    (R1 R2 : K → A → B → Prop) (P1 P2 : K → A → Prop) (Q1 Q2 : K → B → Prop)
+    (IffR : ∀ k a b, R1 k a b ↔ R2 k a b) (IffP : ∀ k a, P1 k a ↔ P2 k a) (IffQ : ∀ k b, Q1 k b ↔ Q2 k b)
     (m1 : M A) (m2 : M B) :
   map_relation R1 P1 Q1 m1 m2 ↔ map_relation R2 P2 Q2 m1 m2.
 Proof.
@@ -23,7 +23,7 @@ Definition to_max_prefix_list_list {A} (l : list (list A)) : max_prefix_list_lis
   to_max_prefix_list <$> map_seq 0 l.
 Global Instance: Params (@to_max_prefix_list_list) 1 := {}.
 
-Definition prefixes {A} : relation (list (list A)) := map_included prefix.
+Definition prefixes {A} : relation (list (list A)) := map_included (λ _, prefix).
 
 Infix "`prefixes_of`" := prefixes (at level 70) : stdpp_scope.
 
@@ -106,7 +106,7 @@ Section max_prefix_list_list.
 
   Local Lemma to_max_prefix_list_list_includedN_aux n ll1 ll2 :
     to_max_prefix_list_list ll1 ≼{n} to_max_prefix_list_list ll2 →
-    map_included (λ l1 l2, l2 ≡{n}≡ l1 ++ drop (length l1) l2) ll1 ll2.
+    map_included (λ _ l1 l2, l2 ≡{n}≡ l1 ++ drop (length l1) l2) ll1 ll2.
   Proof.
     rewrite lookup_includedN => H.
     rewrite /map_included /map_relation => i. move: {H}(H i).
@@ -120,7 +120,7 @@ Section max_prefix_list_list.
   Qed.
   Lemma to_max_prefix_list_list_includedN n ll1 ll2 :
     to_max_prefix_list_list ll1 ≼{n} to_max_prefix_list_list ll2
-    ↔ map_included (λ l1 l2, ∃ l, l2 ≡{n}≡ l1 ++ l) ll1 ll2.
+    ↔ map_included (λ _ l1 l2, ∃ l, l2 ≡{n}≡ l1 ++ l) ll1 ll2.
   Proof.
     split.
     - intros H%to_max_prefix_list_list_includedN_aux i. move: {H}(H i).
@@ -134,7 +134,7 @@ Section max_prefix_list_list.
   Qed.
   Lemma to_max_prefix_list_list_included ll1 ll2 :
     to_max_prefix_list_list ll1 ≼ to_max_prefix_list_list ll2
-    ↔ map_included (λ l1 l2, ∃ l, l2 ≡ l1 ++ l) ll1 ll2.
+    ↔ map_included (λ _ l1 l2, ∃ l, l2 ≡ l1 ++ l) ll1 ll2.
   Proof.
     split.
     - intros IN i.
@@ -244,7 +244,7 @@ Section mono_list_list.
   Qed.
 
   Lemma mono_list_list_both_validN n ll1 ll2 :
-    ✓{n} (●MLL ll1 ⋅ ◯MLL ll2) ↔ map_included (λ l1 l2, ∃ l, l2 ≡{n}≡ l1 ++ l) ll2 ll1.
+    ✓{n} (●MLL ll1 ⋅ ◯MLL ll2) ↔ map_included (λ _ l1 l2, ∃ l, l2 ≡{n}≡ l1 ++ l) ll2 ll1.
   Proof.
     rewrite /mono_list_list_auth /mono_list_list_lb -assoc
       -auth_frag_op auth_both_validN -to_max_prefix_list_list_includedN.
@@ -258,7 +258,7 @@ Section mono_list_list.
   Qed.
 
   Lemma mono_list_list_both_valid ll1 ll2 :
-    ✓ (●MLL ll1 ⋅ ◯MLL ll2) ↔ map_included (λ l1 l2, ∃ l, l2 ≡ l1 ++ l) ll2 ll1.
+    ✓ (●MLL ll1 ⋅ ◯MLL ll2) ↔ map_included (λ _ l1 l2, ∃ l, l2 ≡ l1 ++ l) ll2 ll1.
   Proof.
     rewrite /mono_list_list_auth /mono_list_list_lb -assoc -auth_frag_op
       auth_both_valid -max_prefix_list_list_included_includedN