Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into...

Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a [Hint Resolve], so that the opaqueness annotations are not ignored.

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.

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.

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.

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 :

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.