From ac8d57a0394ad3bbbd978c480a215701d33d5131 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.
---
opam | 2 +-
theories/lang/lifting.v | 2 +-
theories/lang/proofmode.v | 4 ++--
theories/typing/base.v | 8 +++++++-
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 ----
9 files changed, 16 insertions(+), 14 deletions(-)
diff --git a/opam b/opam
index 224547ed..a958ad4a 100644
--- a/opam
+++ b/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") }
]
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 4bac7690..2daa85ad 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,8 +1,8 @@
+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.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 223518ce..ef5c8bd7 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,8 +1,8 @@
-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.
diff --git a/theories/typing/base.v b/theories/typing/base.v
index c04533a9..f5a8b002 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,6 +1,12 @@
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.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index f1df0427..c92f87bd 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 3512082b..53a3a252 100644
--- a/theories/typing/lib/spawn.v
+++ b/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} :
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 2b631d86..860b1c07 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,6 +1,6 @@
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.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 7280e94c..f55191b3 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.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 :
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 5b61f4b5..bee83efc 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 defintion of delete for
- sets coming from the prelude. *)
-From lrust.lang Require Export new_delete.
--
GitLab