Fix build : forgot a file. Also, some tweaks to simplify the proofs.

theories/typing/cont.v

@@ -8,7 +8,7 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  Lemma type_jump E L C T k args T' :
+  Lemma type_jump args E L C T k T' :
     (k ◁cont(L, T'))%CC ∈ C →
     tctx_incl E L T (T' (list_to_vec args)) →
     typed_body E L C T (k (of_val <$> args)).

theories/typing/own.v

@@ -235,9 +235,9 @@ Section typing.
   Qed.
 
   Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
-    ty.(ty_size) = 1%nat →
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
+    ty.(ty_size) = 1%nat →
     (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x := p in e).
   Proof.

theories/typing/tests/get_x.v

@@ -23,6 +23,6 @@ Section get_x.
       intros p'; simpl_subst.
     eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.
-    eapply type_jump with (args := [r]); solve_typing.
+    eapply (type_jump [_]); solve_typing.
   Qed.
 End get_x.

theories/typing/tests/rebor.v

+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition rebor :=
+    (funrec: <> ["t1"; "t2"] :=
+       Newlft;;
+       letalloc: "x" := "t1" in
+       let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
+       "x" <- "t2";;
+       let: "y'" := !"y" in
+       letalloc: "r" := "y'" in
+       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
+                 delete [ #1; "x"] ;; "return" ["r":expr])%E.
+
+  Lemma rebor_type :
+    typed_instruction_ty [] [] [] rebor
+        (fn (λ _, []) (λ _, [# own 2 (Π[int; int]); own 2 (Π[int; int])])
+            (λ (_ : ()), own 1 int)).
+  Proof.
+    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
+    eapply (type_newlft []). apply _. move=> α.
+    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); (try solve_typing)=>x. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
+    eapply (type_letpath (&uniq{α}int)); (try solve_typing)=>y. simpl_subst.
+    eapply (type_assign _ (&uniq{α}Π [int; int])); try solve_typing. by apply write_own.
+    eapply type_deref; try solve_typing; [apply: read_uniq; solve_typing|done|]=>y'.
+      simpl_subst.
+    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
+    eapply type_endlft; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End rebor.