8.16-compat

.gitlab-ci.yml

@@ -56,7 +56,7 @@ trigger-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.15.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.16.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
     refs:

theories/typing/fixpoint.v

@@ -61,7 +61,7 @@ Section fixpoint.
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
       + apply bi.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl, bi.limit_preserving_entails;
+      + apply limit_preserving_impl', bi.limit_preserving_entails;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 

theories/typing/lib/cell.v

@@ -209,7 +209,7 @@ Section typing.
     iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
     (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
     wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
-    { by rewrite Heq. }
+    { rewrite Heq /= ?Nat2Z.id //. }
     { f_equal. done. }
     iIntros "[Hr↦ Hc'↦]". wp_seq.
     iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
@@ -225,7 +225,7 @@ Section typing.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
       - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
-      - iFrame. iExists _. iFrame. }
+      - try rewrite !Nat2Z.id. iFrame. iExists _. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.