No longer depend on Export bugs.

opam

@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-08-29.2.b75bb397") | (= "dev") }
+  "coq-iris" { (= "dev.2019-09-13.1.708b8ac0") | (= "dev") }
 ]

theories/lang/lifting.v

+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang heap.
 From lrust.lang Require Import tactics.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/lang/proofmode.v

-From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
-From lrust.lang Require Export tactics lifting.
+From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting.
+From lrust.lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/typing/base.v

 From lrust.lang Require Export proofmode.
 From lrust.lifetime Require Export frac_borrow.
 
+(* Last, so that we make sure we shadow the defintion of delete for
+   sets coming from the prelude. *)
+From lrust.lang.lib Require Export new_delete.
+
+Open Scope Z_scope.
+
 Create HintDb lrust_typing.
 Create HintDb lrust_typing_merge.
 
@@ -28,4 +34,4 @@ Hint Resolve <- elem_of_app : lrust_typing.
 (* done is there to handle equalities with constants *)
 Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
 Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
\ No newline at end of file
+Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.

theories/typing/lib/join.v

@@ -21,7 +21,7 @@ Section join.
                             letcall: "r" := "call_once_A" ["fA"]%E in
                             finish ["c"; "r"]] in
       letcall: "retB" := "call_once_B" ["fB"]%E in
-      let: "retA" := join ["join"] in
+      let: "retA" := spawn.join ["join"] in
       (* Put the results in a pair. *)
       let: "ret" := new [ #(R_A.(ty_size) + R_B.(ty_size)) ] in
       "ret" +ₗ #0 <-{R_A.(ty_size)} !"retA";;

theories/typing/lib/spawn.v

@@ -110,7 +110,7 @@ Section spawn.
   Definition join : val :=
     funrec: <> ["c"] :=
       let: "c'" := !"c" in
-      let: "r" := join ["c'"] in
+      let: "r" := spawn.join ["c'"] in
       delete [ #1; "c"];; return: ["r"].
 
   Lemma join_type retty `{!TyWf retty} :

theories/typing/lib/swap.v

 From iris.proofmode Require Import tactics.
-From lrust.typing Require Import typing.
 From lrust.lang.lib Require Import swap.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section swap.

theories/typing/own.v

 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From lrust.lang.lib Require Import new_delete memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
@@ -254,7 +254,7 @@ Section typing.
     iApply wp_new; try done. iModIntro.
     iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length. 
+    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length.
   Qed.
 
   Lemma type_new {E L C T} (n' : nat) x (n : Z) e :

theories/typing/typing.v

@@ -3,7 +3,3 @@ From lrust.typing Require Export
   lft_contexts type_context cont_context programs cont type
   int bool own uniq_bor shr_bor uninit product sum fixpoint function
   product_split borrow type_sum.
-
-(* Last, so that we make sure we shadow the defintion of delete for
-   sets coming from the prelude. *)
-From lrust.lang Require Export new_delete.