diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 33661cdcf019b28f32596588d939ecffd3b1c115..29679d766fa20692f6a115f6353621eccb03eaef 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -29,9 +29,8 @@ Section lazy_lft.
     iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
     iApply type_int. iIntros (v42). simpl_subst.
     iApply type_assign; [solve_typing|by eapply write_own|].
-    (* FIXME somehow this fails nowadays if we don't give the own_ptr hints. *)
-    iApply (type_assign (own_ptr _ _) (&shr{α} _)); [solve_typing..|by eapply write_own|].
-    iApply (type_assign (own_ptr _ _)); [solve_typing|by eapply write_own|].
+    iApply (type_assign _ (&shr{α} _)); [solve_typing..|by eapply write_own|].
+    iApply type_assign; [solve_typing|by eapply write_own|].
     iApply type_deref; [solve_typing|apply: read_own_copy|done|]. iIntros (t0'). simpl_subst.
     iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
     iApply type_int. iIntros (v23). simpl_subst.
@@ -39,10 +38,7 @@ Section lazy_lft.
     iApply (type_assign _ (&shr{α} int)); [solve_typing..|by eapply write_own|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_endlft; [solve_typing..|].
-    iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T).
-    { (* FIXME how on earth has this ever worked? It's also really slow even now. *)
-      eapply tctx_extract_merge_own_prod; first done. solve_typing. }
-    { solve_typing. } { solve_typing. }
+    iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 755b290eb8155a480804f9bebe37fdc9c38473c7..78a3b34bb03cbbe912d21e8341e296fc7b5648b3 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -19,8 +19,7 @@ Section unbox.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
     iIntros (b'); simpl_subst.
     iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
-    (* FIXME: For some reason, Coq prefers to type this as &shr{α}. *)
-    iApply (type_letalloc_1 (&uniq{α} _)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/option.v b/theories/typing/option.v
index 6c95105cb5a77091bd94c3f66e8a4d8902adafd3..7aea21c9fbdea20b00fc61908941eca7dcf5b5a1 100644
--- a/theories/typing/option.v
+++ b/theories/typing/option.v
@@ -59,10 +59,7 @@ Section option.
       iApply (type_jump [_]); solve_typing.
     + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
         simpl_subst.
-      iApply (type_delete (Π[uninit _;uninit _;uninit _])).
-      { (* FIXME how on earth has this ever worked? *)
-        eapply tctx_extract_merge_own_prod; first done. solve_typing. }
-      { solve_typing. } { solve_typing. }
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 2f8543c503cdd24a6822f99f8215165c6238db6a..464fcf86b4893b61db931a790d7038b27b49ca50 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -164,7 +164,7 @@ Section box.
 
   Global Instance box_mono E L :
     Proper (subtype E L ==> subtype E L) box.
-  Proof.    
+  Proof.
     intros ty1 ty2 Hincl. iIntros. iApply box_type_incl. iApply Hincl; auto.
   Qed.
   Lemma box_mono' E L ty1 ty2 :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 4cd8f82d7116c24942a8f3d3d64f1336df30ed8c..92ef13e3e0da06335ed04899ac9f69f6eb3824fd 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -346,8 +346,5 @@ Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
 (* In general, we want reborrowing to be tried before subtyping, so
    that we get the extraction. However, in the case the types match
    exactly, we want to NOT use reborrowing. Therefore, we add
-   [tctx_extract_hasty_here_eq] as a hint with a very low cost.
-   Furthermore, we add it as an external hint to get better unification
-   behavior. *)
-Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
-  apply tctx_extract_hasty_here_eq : lrust_typing.
+   [tctx_extract_hasty_here_eq] as a hint with a very low cost. *)
+Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.