Fix build.

theories/typing/borrow.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
-From lrust.typing Require Export uniq_bor shr_bor own sum.
+From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in

theories/typing/sum.v

@@ -123,11 +123,11 @@ Section sum.
         by iApply (Hty2 with "* [] []"). }
     clear -Hleq. iSplit; last iSplit.
     - simpl. by rewrite Hleq.
-    - iNext. iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
       iSplit; first by rewrite -Hleq.
       iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
-    - iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+    - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
       iExists i. iSplitR "Hshr".
       + rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
         iDestruct "Hlen" as %<-. done.