fix

_CoqProject

@@ -8,6 +8,8 @@
 -arg -w -arg -redundant-canonical-projection
 # we use Restart for demoing purposes, sometimes
 -arg -w -arg -undo-batch-mode
+# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
 
 # library stuff
 theories/lib/maps.v

semantics.opam

@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.20" & < "8.21~") | (= "dev") }
   "coq-iris-heap-lang" { (= "dev.2024-12-06.1.72e683c9") | (= "dev") }
-  "coq-equations" { (= "1.3+8.19") | (= "1.3+8.20") }
-  "coq-autosubst" { (= "1.8") | (= "dev") }
+  "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") }
+  "coq-autosubst" { (= "1.9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/program_logics/program_logic/adequacy.v

@@ -48,7 +48,7 @@ Proof.
   iApply (step_fupd_wand with "H"). iIntros ">($ & He2 & -> & ->) !>".
   rewrite !app_nil_r; iFrame.
   iPureIntro; split; first done.
-  rewrite !app_length; simpl; lia.
+  rewrite !length_app; simpl; lia.
 Qed.
 
 Lemma wptp_steps s n es1 es2 κs σ1 σ2 Φs :