From 9169334126a4abb3ea2889b952e95d160d58df40 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 17 Oct 2023 10:02:34 +0200
Subject: [PATCH] update dependencies
---
coq-gpfsl.opam | 2 +-
gpfsl-examples/algebra/mono_list_list.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 61db5e55..1d0498b0 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.2023-10-16.0.4a17223a") | (= "dev") }
+ "coq-iris" { (= "dev.2023-10-16.2.5e58df61") | (= "dev") }
"coq-orc11" {= version}
]
diff --git a/gpfsl-examples/algebra/mono_list_list.v b/gpfsl-examples/algebra/mono_list_list.v
index db2dc675..9dd054f2 100644
--- a/gpfsl-examples/algebra/mono_list_list.v
+++ b/gpfsl-examples/algebra/mono_list_list.v
@@ -173,7 +173,7 @@ Section max_prefix_list_list.
rewrite /to_max_prefix_list_list !fmap_map_seq !lookup_map_seq Nat.sub_0_r !list_lookup_fmap.
rewrite !option_guard_True; [|lia..].
destruct oll as [ll|]; simpl; last by rewrite !right_id.
- destruct (ll !! i) as [l|]; simpl; last by rewrite !right_id.
+ destruct (ll !! i) as [l|] eqn:EQll; rewrite EQll /=; last by rewrite !right_id.
destruct (ll1 !! i) as [l1|], (ll2 !! i) as [l2|]; simpl; [|done| |done].
- rewrite -!Some_op. intros P V EQ%Some_dist_inj. f_equiv.
move: (max_prefix_list_local_update l1 l2 P n (Some l)). naive_solver.
--
GitLab