From c1dba5730edb0ead570fe4598e49722f2ba0f2c1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 13 Sep 2019 20:10:25 +0200
Subject: [PATCH] No longer depend on Export bugs.

---
 theories/typing/base.v      | 6 ++++++
 theories/typing/lib/join.v  | 2 +-
 theories/typing/lib/spawn.v | 2 +-
 theories/typing/lib/swap.v  | 2 +-
 theories/typing/own.v       | 4 ++--
 theories/typing/typing.v    | 4 ----
 6 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/theories/typing/base.v b/theories/typing/base.v
index 64cb2927..796d2243 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,6 +1,12 @@
 From lrust.lifetime Require Export frac_borrow.
 From gpfsl.base_logic Require Import na.
 
+(* Last, so that we make sure we shadow the definition 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.
 
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 3c011691..c6a3fd72 100644
--- a/theories/typing/lib/join.v
+++ b/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";;
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 4ca1c03d..772d602e 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -113,7 +113,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} :
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 161efa5e..d5fc5b15 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,5 +1,5 @@
-From lrust.typing Require Import typing.
 From lrust.lang Require Import swap.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section swap.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index d73f2950..3bed184b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,6 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From lrust.lang Require Import new_delete memcpy.
+From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
@@ -255,7 +255,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 :
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index ea4c662d..45a4fa08 100644
--- a/theories/typing/typing.v
+++ b/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 definition of delete for
-   sets coming from the prelude. *)
-From lrust.lang Require Export new_delete.
-- 
GitLab