Fix build.

theories/typing/function.v

@@ -209,7 +209,7 @@ Section typing.
     intros Hfn HE HTT' HC HT'T''.
     rewrite -typed_body_mono /flip; last done; first by eapply type_call.
     - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
-      apply cctx_incl_cons; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
+      apply cctx_incl_cons_match; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
     - etrans; last by apply (tctx_incl_frame_l _ _ [_]).
       apply copy_elem_of_tctx_incl; last done. apply _.
   Qed.

theories/typing/lft_contexts.v

@@ -436,9 +436,9 @@ Hint Resolve
 (* We declare these as hint extern, so that the [B] parameter of elem_of does
    not have to be [list _] and can be an alias of this. *)
 Hint Extern 0 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
-  eapply @elem_of_list_here.
+  eapply @elem_of_list_here : lrust_typing.
 Hint Extern 1 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
-  eapply @elem_of_list_further.
+  eapply @elem_of_list_further : lrust_typing.
 
 Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.