From aa0081c540dd736e9ab16e1735281f9127f23e80 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 12 Aug 2022 17:45:08 -0400 Subject: [PATCH] 8.16-compat --- .gitlab-ci.yml | 2 +- theories/typing/fixpoint.v | 2 +- theories/typing/lib/cell.v | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 902af482..cb3d556b 100644 --- a/.gitlab-ci.yml +++ b/.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: diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v index a8df5832..5fc548e9 100644 --- a/theories/typing/fixpoint.v +++ b/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. diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v index f4325de4..3b0284d8 100644 --- a/theories/typing/lib/cell.v +++ b/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. -- GitLab