From 03fdb63e6554bb30deefeda8e69eff554e0e55df Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 4 Mar 2017 23:49:11 +0100
Subject: [PATCH] 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 | 10 +++-------
 theories/typing/examples/unbox.v    |  3 +--
 theories/typing/option.v            |  5 +----
 theories/typing/own.v               |  2 +-
 theories/typing/type_context.v      |  7 ++-----
 5 files changed, 8 insertions(+), 19 deletions(-)

diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 33661cdc..29679d76 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 755b290e..78a3b34b 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 6c95105c..7aea21c9 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 2f8543c5..464fcf86 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 4cd8f82d..92ef13e3 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.
-- 
GitLab