Compare revisions

0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,7 +3,4 @@ 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.
+From iris.prelude Require Import options.
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
--- a/lifetime/meta.v
+++ b/lifetime/meta.v
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
No results found