diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4f59879efed3d959a7c6f82895d98c7070ec9f08..07d8b2a736e0e2d9ce0c6b439a8bc7e899dbdf7f 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 4262b17c62f5650dbc137e687443faa17f83e620..93ce17427217d6b3e032e09aa889e473ea6ea5c2 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 8c7903132ff9418f06f4eac4422db16624ee4327..03c0c62d7cac005b61d169cbb6c135c7375a3646 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 a1408fa414e438d0291975ef07e85cf3032f517f..03d565f084a94950e90161725fe087aa068bb9d6 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.