diff --git a/theories/typing/function.v b/theories/typing/function.v
index b09e8af19d3c4cdce5a834ec74a6f9f55d3517fb..2182ff1acf7633b0d9af062e075a0d14a127ad1d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
 
-  Record fn_params := FP { fp_tys : vec type n; fp_ty : type; fp_E : elctx }.
+  Record fn_params := FP' { fp_tys : vec type n; fp_ty : type; fp_E : elctx }.
 
   Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
@@ -47,7 +47,7 @@ Section fn.
   Proof. intros ?? HR. apply HR. Qed.
 
   Global Instance FP_proper R :
-    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==> eq ==> fn_params_rel R) FP.
+    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==> eq ==> fn_params_rel R) FP'.
   Proof. by split; [|split]. Qed.
 
   Global Instance fn_type_contractive n' :
@@ -98,11 +98,11 @@ End fn.
 
 Arguments fn_params {_ _} _.
 
-(* The parameter of [FP] are in the wrong order in order to make sure
+(* The parameter of [FP'] are in the wrong order in order to make sure
    that type-checking is done in that order, so that the [ELCtx_Alive]
    is taken as a coercion. We reestablish the intuitive order with
-   [FP'] *)
-Notation FP' E tys ty := (FP tys ty E).
+   [FP] *)
+Notation FP E tys ty := (FP' tys ty E).
 
 (* We use recursive notation for binders as well, to allow patterns
    like '(a, b) to be used. In practice, only one binder is ever used,
@@ -112,19 +112,19 @@ Notation FP' E tys ty := (FP tys ty E).
    printing. Once on 8.6pl1, this should work.  *)
 Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ x, (.. (λ x',
-      FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
+      FP E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
-  (fn (λ x, (.. (λ x', FP' E%EL Vector.nil R%T)..)))
+  (fn (λ x, (.. (λ x', FP E%EL Vector.nil R%T)..)))
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
-  (fn (λ _:(), FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
+  (fn (λ _:(), FP E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
   (at level 99, R at level 200,
    format "'fn(' E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ')' '→' R" :=
-  (fn (λ _:(), FP' E%EL Vector.nil R%T))
+  (fn (λ _:(), FP E%EL Vector.nil R%T))
   (at level 99, R at level 200,
    format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index c1012db9e85a6547a405cad6804de80b72e5f486..1799970be091d82f24e52eee5eae3003d46000eb 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -56,7 +56,7 @@ Section ref_functions.
      See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty :
     typed_val ref_clone
-      (fn (fun '(α, β) => FP' [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+      (fn (fun '(α, β) => FP [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 8c6fd2351e90af488c32071ee188e05e3cff6be5..a9534a10e51930405315fe9e7f6971ba851c2db7 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,7 +20,7 @@ Section refmut_functions.
 
   Lemma refmut_deref_type ty :
     typed_val refmut_deref
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -60,7 +60,7 @@ Section refmut_functions.
 
   Lemma refmut_derefmut_type ty :
     typed_val refmut_derefmut
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
                               (&uniq{α}ty)%T)).
    Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index c2eaab6779ab658e48c8efbb1cead75bd23504ee..353f6b7215815afc23ad4543e1ae62175832b6b9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,7 +20,7 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
                               [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 0ebe26120cc2200c39602b83bc33c2b6eb33e077..68741c9e7c2204cac8d3abebcd6bc94c233cd2b5 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,7 +20,7 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
                               [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -62,7 +62,7 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
                               [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index e19b166b782ef60d39631fe302502b7a7ba0bf86..390d44c3ce478a14e5f56bbc8ccf1922e56a2ce6 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -84,7 +84,7 @@ Section spawn.
         iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
       (* FIXME this is horrible. *)
-      assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP' [] [# envty] retty)).
+      assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP [] [# envty] retty)).
       specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
       erewrite of_val_unlock in Hcall; last done.
       iApply (Hcall $! _ 1%Qp with "LFT Htl [] [] [Hfin]").