From 2e199c32bf1f4e369a3f04f62b9503fc3383866f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Aug 2022 10:27:24 -0400
Subject: [PATCH] use Coq 8.16 for nightly builds, and fix Coq 8.16 build

---
 .gitlab-ci.yml             | 4 ++--
 theories/typing/fixpoint.v | 2 +-
 theories/typing/function.v | 2 +-
 theories/typing/lib/cell.v | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4f59879e..07d8b2a7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,7 +5,7 @@ stages:
 
 variables:
   CPU_CORES: "10"
-  OCAML: "ocaml-base-compiler.4.07.1"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
 
 .template: &template
   stage: build
@@ -43,7 +43,7 @@ trigger-iris.dev:
     IRIS_REPO: "iris/iris"
     ORC11_REPO: "iris/orc11"
     GPFSL_REPO: "iris/gpfsl"
-    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   git+https://gitlab.mpi-sws.org/$ORC11_REPO#$ORC11_REV   git+https://gitlab.mpi-sws.org/$GPFSL_REPO#$GPFSL_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   git+https://gitlab.mpi-sws.org/$ORC11_REPO#$ORC11_REV   git+https://gitlab.mpi-sws.org/$GPFSL_REPO#$GPFSL_REV"
   except:
   only:
   - triggers
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 4262b17c..93ce1742 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/function.v b/theories/typing/function.v
index 8c790313..03c0c62d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -360,7 +360,7 @@ Section typing.
     ⊢ typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HL HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
+    iApply typed_body_mono; [| |done|by iApply type_call']; simpl.
     - etrans.
       + eapply (incl_cctx_incl _ [_]); by intros ? ->%elem_of_list_singleton.
       + apply cctx_incl_cons; first done. intros args. by inv_vec args.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index a1408fa4..03d565f0 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -190,7 +190,7 @@ Section typing.
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (c'); simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply (type_new (ty_size ty)); [solve_typing..|]; iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
     iIntros (tid qmax) "#LFT #HE Htl HL HC".
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-- 
GitLab