From 5fc9f085641c98d836cab3907bb74cede843a1aa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 10:52:49 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                               | 2 +-
 theories/lang/heap.v                               | 2 +-
 theories/lang/lib/arc.v                            | 2 +-
 theories/lang/lib/lock.v                           | 2 +-
 theories/lang/lib/spawn.v                          | 2 +-
 theories/lang/lib/tests.v                          | 2 +-
 theories/lang/lifting.v                            | 2 +-
 theories/lang/proofmode.v                          | 2 +-
 theories/lifetime/at_borrow.v                      | 2 +-
 theories/lifetime/frac_borrow.v                    | 2 +-
 theories/lifetime/lifetime.v                       | 2 +-
 theories/lifetime/meta.v                           | 2 +-
 theories/lifetime/model/accessors.v                | 2 +-
 theories/lifetime/model/borrow.v                   | 2 +-
 theories/lifetime/model/borrow_sep.v               | 2 +-
 theories/lifetime/model/creation.v                 | 2 +-
 theories/lifetime/model/faking.v                   | 2 +-
 theories/lifetime/model/primitive.v                | 2 +-
 theories/lifetime/model/reborrow.v                 | 2 +-
 theories/lifetime/na_borrow.v                      | 2 +-
 theories/typing/bool.v                             | 2 +-
 theories/typing/borrow.v                           | 2 +-
 theories/typing/cont.v                             | 2 +-
 theories/typing/cont_context.v                     | 2 +-
 theories/typing/examples/get_x.v                   | 2 +-
 theories/typing/examples/init_prod.v               | 2 +-
 theories/typing/examples/lazy_lft.v                | 2 +-
 theories/typing/examples/nonlexical.v              | 2 +-
 theories/typing/examples/rebor.v                   | 2 +-
 theories/typing/examples/unbox.v                   | 2 +-
 theories/typing/function.v                         | 2 +-
 theories/typing/int.v                              | 2 +-
 theories/typing/lft_contexts.v                     | 2 +-
 theories/typing/lib/arc.v                          | 2 +-
 theories/typing/lib/brandedvec.v                   | 2 +-
 theories/typing/lib/cell.v                         | 2 +-
 theories/typing/lib/diverging_static.v             | 2 +-
 theories/typing/lib/fake_shared.v                  | 2 +-
 theories/typing/lib/ghostcell.v                    | 2 +-
 theories/typing/lib/join.v                         | 2 +-
 theories/typing/lib/mutex/mutex.v                  | 2 +-
 theories/typing/lib/mutex/mutexguard.v             | 2 +-
 theories/typing/lib/option.v                       | 2 +-
 theories/typing/lib/panic.v                        | 2 +-
 theories/typing/lib/rc/rc.v                        | 2 +-
 theories/typing/lib/rc/weak.v                      | 2 +-
 theories/typing/lib/refcell/ref.v                  | 2 +-
 theories/typing/lib/refcell/ref_code.v             | 2 +-
 theories/typing/lib/refcell/refcell.v              | 2 +-
 theories/typing/lib/refcell/refcell_code.v         | 2 +-
 theories/typing/lib/refcell/refmut.v               | 2 +-
 theories/typing/lib/refcell/refmut_code.v          | 2 +-
 theories/typing/lib/rwlock/rwlock.v                | 2 +-
 theories/typing/lib/rwlock/rwlock_code.v           | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard.v       | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard_code.v  | 2 +-
 theories/typing/lib/rwlock/rwlockwriteguard.v      | 2 +-
 theories/typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
 theories/typing/lib/spawn.v                        | 2 +-
 theories/typing/lib/swap.v                         | 2 +-
 theories/typing/lib/take_mut.v                     | 2 +-
 theories/typing/own.v                              | 2 +-
 theories/typing/product.v                          | 2 +-
 theories/typing/product_split.v                    | 2 +-
 theories/typing/shr_bor.v                          | 2 +-
 theories/typing/soundness.v                        | 2 +-
 theories/typing/sum.v                              | 2 +-
 theories/typing/type_context.v                     | 2 +-
 theories/typing/type_sum.v                         | 2 +-
 theories/typing/uninit.v                           | 2 +-
 theories/typing/uniq_bor.v                         | 2 +-
 theories/typing/util.v                             | 2 +-
 72 files changed, 72 insertions(+), 72 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index c8e90773..e968f4f3 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-07-23.2.572da574") | (= "dev") }
+  "coq-iris" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 306a6de4..f77770c1 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import big_op gmap frac agree numbers.
 From iris.algebra Require Import csum excl auth cmra_big_op.
 From iris.bi Require Import fractional.
 From iris.base_logic Require Export lib.own.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From lrust.lang Require Export lang.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 528ea5c1..8b400fd5 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi Require Import fractional.
 From iris.algebra Require Import excl csum frac auth numbers.
 From lrust.lang Require Import lang proofmode notation new_delete.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 364aba41..2ab7a9f3 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index c603babc..66ad5d22 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import weakestpre.
 From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import proofmode notation.
 From lrust.lang Require Export lang.
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 82b76da0..7f6ebbaa 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 38567f42..ba10d822 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang heap.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 3ea0ab9f..b38d166f 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import coq_tactics reduction.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting.
 From lrust.lang Require Export tactics lifting.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 84d0c052..7fef53b3 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lifetime Require Export lifetime.
 Set Default Proof Using "Type".
 
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6c88d97e..07561dde 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi Require Import fractional.
 From iris.algebra Require Import frac.
 From lrust.lifetime Require Export at_borrow.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 1a8a9b3a..bfa1040c 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -1,7 +1,7 @@
 From lrust.lifetime Require Export lifetime_sig.
 From lrust.lifetime.model Require definitions primitive accessors faking borrow
      borrow_sep reborrow creation.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Module Export lifetime : lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 5872acd5..f5d8f12e 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import dyn_reservation_map agree.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lifetime Require Export lifetime.
 Set Default Proof Using "Type".
 
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index ac80399c..49d61adb 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Export primitive.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index aea3fa11..ebfce718 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Section borrow.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index e01b8f51..47dbef7d 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking reborrow.
 From iris.algebra Require Import csum auth frac gmap agree.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Section borrow.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index e9dd05da..1bab34a2 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Section creation.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 1500524e..861262c3 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,7 +1,7 @@
 From lrust.lifetime Require Export primitive.
 From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Section faking.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 798d8d0e..b7f6c4db 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -2,7 +2,7 @@ From lrust.lifetime.model Require Export definitions.
 From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classes.
 From iris.base_logic.lib Require Import boxes.
 From iris.bi Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 3f990264..1c38d82a 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,7 +1,7 @@
 From lrust.lifetime Require Import borrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Section reborrow.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 729cc576..cd77e700 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export lifetime.
 From iris.base_logic.lib Require Export na_invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 6c1e4f83..4e2dfb0b 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index ad909c54..2f7a11b4 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 1cca2081..fb437c5d 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index ff78d9db..cd3ca83b 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 95486f6e..a23415e6 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index ee0bc5ba..d4c2e6f5 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index b9bf7354..1dbeee54 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 2718f2e8..617eed75 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing lib.option.
 
 (* Typing "problem case #3" from:
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 4b5cda26..b8c0b033 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index b1a13d01..1909c781 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index cba36f42..9a7711fd 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import vector list.
 From lrust.typing Require Export type.
 From lrust.typing Require Import own programs cont.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 4ec16f6d..94771e2f 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import bool programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 0dc89dcf..f4383a45 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi Require Import fractional.
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export base.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index b1dcc976..ff2a94ad 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy arc.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 979b61d8..67af8d85 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import auth numbers.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import proofmode notation lib.new_delete.
 From lrust.lifetime Require Import meta.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 104a1a2c..0e343ad8 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index abbedcab..6ca1456e 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index d10fe83f..9756ed20 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index b66130a0..43660eb0 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import csum frac excl agree coPset.
 From iris.bi Require Import lib.fractional.
 From lrust.lang Require Import proofmode notation.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index fc593c24..05f87157 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 65bbe7f9..95bb5d5f 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 6ee38f83..5aea0ab2 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 6f7a4b5f..1cde437f 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing lib.panic.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index fe40d55b..c3155163 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 10c15e91..ae5bb607 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree excl numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index b9ad6cd0..c1fab158 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index cd37e6b8..c8b40966 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 9df46b27..58a897fa 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 7ccd3888..5e309dbc 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index a4e20122..6de85bb7 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 2549cc0d..fd465bbd 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 680c7d77..18eea9e8 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 77130248..fc2380ea 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree excl numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2f0f3fcf..85344026 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d4741c21..66605b0d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 4cd8f7ca..1b553acc 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 620afee4..925a746f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index beda5f49..ab0daec5 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 6fc0af6b..c8b96eb3 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index d920a7d2..30590962 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import swap.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 8c9f2155..893f70ae 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c0db77cf..822223da 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 57e1e108..82ec0d17 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list numbers.
 From lrust.typing Require Import lft_contexts.
 From lrust.typing Require Export type.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 150710d3..70601228 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import numbers.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
 From lrust.typing Require Import shr_bor.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 360c9672..cebbcef5 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 4ef123dc..ebe28593 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import frac.
 From iris.base_logic.lib Require Import na_invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import races adequacy proofmode notation.
 From lrust.lifetime Require Import lifetime frac_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 0bfaa42a..c124981f 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.bi Require Import fractional.
 From lrust.typing Require Import lft_contexts.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 45da5647..01e52295 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 4bb4ab17..4d2212e5 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 23637fd5..ee81c610 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import product.
 Set Default Proof Using "Type".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 742c8c95..113f50ea 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util lft_contexts type_context programs.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 5edf38b7..e2489c01 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
-- 
GitLab