bump

_CoqProject

@@ -63,6 +63,7 @@ theories/type_systems/systemf_mu_state/locations.v
 theories/type_systems/systemf_mu_state/lang.v
 theories/type_systems/systemf_mu_state/notation.v
 theories/type_systems/systemf_mu_state/types.v
+theories/type_systems/systemf_mu_state/types_sol.v
 theories/type_systems/systemf_mu_state/tactics.v
 theories/type_systems/systemf_mu_state/execution.v
 theories/type_systems/systemf_mu_state/parallel_subst.v
@@ -106,7 +107,8 @@ theories/program_logics/logrel/ghost_state.v
 # resources
 theories/program_logics/ra_lib.v
 theories/program_logics/resource_algebras_1.v
-#theories/program_logics/resource_algebras_2.v
+theories/program_logics/resource_algebras_2.v
+theories/program_logics/resource_algebras_sol.v
 
 theories/program_logics/fupd.v
 
@@ -122,17 +124,28 @@ theories/program_logics/reloc/fundamental.v
 theories/program_logics/reloc/adequacy.v
 theories/program_logics/reloc/contextual_refinement.v
 
+theories/program_logics/reloc_sol/ghost_state.v
+theories/program_logics/reloc_sol/src_rules.v
+theories/program_logics/reloc_sol/persistent_bipred.v
+theories/program_logics/reloc_sol/notation.v
+theories/program_logics/reloc_sol/proofmode.v
+theories/program_logics/reloc_sol/syntactic.v
+theories/program_logics/reloc_sol/logrel.v
+theories/program_logics/reloc_sol/fundamental.v
+theories/program_logics/reloc_sol/adequacy.v
+theories/program_logics/reloc_sol/contextual_refinement.v
 
 # concurrency
 theories/program_logics/concurrency.v
 theories/program_logics/concurrent_logrel/syntactic.v
 theories/program_logics/concurrent_logrel/logrel.v
+theories/program_logics/concurrent_logrel/logrel_sol.v
 theories/program_logics/concurrent_logrel/adequacy.v
 
-
 # By removing the # below, you can add the exercise sheets to make
 # <comment-out>
 theories/type_systems/warmup/warmup.v
+theories/type_systems/warmup/warmup_sol.v
 theories/type_systems/stlc/exercises01.v
 theories/type_systems/stlc/exercises02.v
 theories/type_systems/stlc/cbn_logrel.v
@@ -141,4 +154,5 @@ theories/type_systems/systemf/exercises04.v
 theories/type_systems/systemf/exercises05.v
 theories/type_systems/systemf_mu/exercises06.v
 theories/type_systems/systemf_mu_state/exercises07.v
+theories/type_systems/systemf_mu_state/exercises07_sol.v
 # </comment-out>

semantics.opam

@@ -9,9 +9,9 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2024-08-20.0.657b34ad") | (= "dev") }
-  "coq-equations" { (= "1.3+8.18") | = "1.3+8.19" }
+  "coq" { (>= "8.19" & < "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") }
 ]
 

theories/program_logics/program_logic/adequacy.v

@@ -94,7 +94,7 @@ Proof.
   iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
   iModIntro. iApply (step_fupdN_wand with "Hwp").
   iMod 1 as "(Hσ & Ht & $ & $)"; simplify_eq/=.
-  iMod (fupd_plain_keep_l ∅
+  iMod (fupd_plain_keep_l _ ∅
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
     (state_interp σ2 ∗
      wptp s es2 (Φs))%I