diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index c8e90773c245b008c6f5c39d7b2af5fa1247c75f..e968f4f318e978ca46692f42d9862a0154d40adf 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 306a6de47b70c3ac7ccf20f0c4184893dbf93484..f77770c13513913e317dc3ec0fce8a4eb69f5353 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 528ea5c1d1062497329021d7c0635a59b44ddea8..8b400fd551a8937d4d89a970e42ea103eee72c0c 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 364aba416eef07415e5ce51a71b1d3352260fe29..2ab7a9f3f0c0aa08f0cba8b1b8cac26135b43dbf 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 c603babc0e1e536d7768f5f7a1dc606e607a5aca..66ad5d229099a19ad7fcb1a0903d8fc67c96fcdd 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 82b76da0b124113df8fad871355698db48fafc39..7f6ebbaa0151d64058862dab062f01b6dec2ec40 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 38567f42bd18b6d71a39355e308b7c114c0274c2..ba10d822749bf0cdf5c859f1fd3d5fa17af104f7 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 3ea0ab9ffe59f7a13e8db77f598a887add0a8687..b38d166f8c059b0d6c2d1bbf0e18132cc2bfdc01 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 84d0c0522919de659ac0242f734fcabe7aa86ac6..7fef53b36bce3dca1427af347500c54b3843ec6b 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 6c88d97e2c921b0ed8e6aa484e4c207d7f1ad646..07561dde3a28376bd58f7b2547b51d3eef57137e 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 1a8a9b3a2e6e1eb0fb71ac868c404f965f788d5b..bfa1040c95c90daf07d9679d08c04a0c6f9330e2 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 5872acd56e05188d8bb16032f86b94dc62ac0b3e..f5d8f12e2e7ca795a553dc435642257eb0896cae 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 ac80399c4f92d3a5752589d12748750f76359b9f..49d61adbf9ab36fe9241d9f06e53d545e15c6bc2 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 aea3fa114016378ea5dc7e9d609da77b7064c137..ebfce718d1f189646f5ebda45d4ef18410f2152e 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 e01b8f518a517194562f3786323ae78f66823b56..47dbef7d4de0abf7b0710f736923520d50830519 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 e9dd05da2363a31baffc7a6344ad98b2f539f993..1bab34a2a440990cfa3a52eaa4c631e028f93545 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 1500524e90b6687b7344de1fa65c5ba1215ec51b..861262c35b34ae5e618afc7fa7ef2886b1b4f5a6 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 798d8d0e94ed7c918be8dfeadd91f92f6cba8529..b7f6c4db72754d912e5949f1ad28543c682f297f 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 3f990264ec09e298217a760dad36a99d41bb69d6..1c38d82a82509798a2ba973dc6b784cee0d11da5 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 729cc5769fbbd8b0a182454966879e5bb80b16c1..cd77e70042496c97f4c2f526e445f47c77571043 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 6c1e4f83df9331980d98f059374b9d91c8f7cf3f..4e2dfb0bc29051fbfdb4bcb4df1fd38a4851580b 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 ad909c549e8ea04d0720504cdf0dad706f5f7614..2f7a11b40ffeabe024b730994bfaa25ce6a9ae28 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 1cca20812ebe4d7115550c9c0e7601894641b6c2..fb437c5d0ef1ac2e15eda429e374dc4df2a9d3ef 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 ff78d9dbf33ced8914c5ebf0206e3e7248416b8e..cd3ca83bc62b155cb6d2c3dcc04a70e7238f31a8 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 95486f6e0a040ad68e5a9fb8854516e00281210c..a23415e6c842b52bb928c7c7ad9f6aa284204db4 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 ee0bc5baad3bb79d6243290226cb38dc6e28e92d..d4c2e6f5f731818c3c978e4f2c6ddd6161e783d6 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 b9bf73543a0f9585f388ee187bab2666f0e2246b..1dbeee546c0c2c059aad2e5fe08d9a3f15f80ae8 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 2718f2e8138fb29a573e2ee524b0c1b4a355416e..617eed75f5b8bde8dbc18a2165fbf2c071dc4f36 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 4b5cda264cbb41f19334a5118cc20f8d3031943d..b8c0b03336ef73584cdc7153ddb04cf46f43001b 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 b1a13d010d4614c49029672d1cbc3cfedbeacc35..1909c78122fc8644490f5176f1ce9cc11d81ce43 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 cba36f427686f98a6106e68a6aaaa86aa7f24bf9..9a7711fd4cd0433e2e2b22500e93ba89aa9bcd50 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 4ec16f6dcaa7a1130470444a4ed8866abd1aaeee..94771e2f8270d883a81f43513ba8ff0c959082d2 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 0dc89dcf2f792ffc81e6a454447232b979efc3bd..f4383a4559b59db1177cdf51da98be9aacc19d76 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 b1dcc9766a3aba7da10f248dee52fc2a7ef8c6c2..ff2a94ade604006a7007b3249346723629f52456 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 979b61d8ede92f7778eeff2febc67dd36ca4df73..67af8d8570086bbc8545b3fb0937958973e388e9 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 104a1a2c750c8e231a77d40bfbca1a120f6482a0..0e343ad815519321247f38e2f0a7397584b405bc 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 abbedcab02b3877b3e34de722c727fd87bc77433..6ca1456e56c87f68ba66a6e924dbc60db9aa2cf6 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 d10fe83f204d0427a8b9caa8881f4c70120a6b4a..9756ed2028a13033c9753c29c0905ae44de8ab16 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 b66130a00108ce592ae3b437d94da2b3958e93ae..43660eb0ee3744ab52e53bb27606f012e70a17eb 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 fc593c245e758395d6910872a0d9dc712d2a4280..05f87157d96974988fdc0bdc2be765782a3b55f4 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 65bbe7f92f4bc873ffaae0a09f935537d1a4fb6c..95bb5d5ff516908ace33feec318d5125a495a141 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 6ee38f834c3be478d41ea43c90a4ba370379e753..5aea0ab2accd7bc2d40b6ccba5324e5beaa926ea 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 6f7a4b5f2df3d66d3191c379340823630da44614..1cde437fb7062da40953da50027f19fa2c3dd734 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 fe40d55b118ff1e3d776951806cd8729cbd76ddb..c3155163ecafe88e48b3baa5a4b2044bf967904c 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 10c15e9128c9c592778940511fe2787902d59d6c..ae5bb6077951a0ca586c524b97f138bd52bf144e 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 b9ad6cd0638e7aa2d41eb41e604526cc5c602c9c..c1fab15832dbb9fe40df0eb9ad51e0b1e7c81687 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 cd37e6b84291e9680b98d8ff0bed2e5f6bbb4d64..c8b4096667e59b5b20b20e9813ecd4fca12a162c 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 9df46b272a58e9c488d908b8a8bf3934f622d053..58a897fa392cfcc410423c520849caf504b387bb 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 7ccd3888213a9c35bc269cf1f5d124f0187e38b9..5e309dbcb32b39d6a0a6abab226143ebcfc5f9ac 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 a4e20122748d4e188c909e6dc68f15224953c4fb..6de85bb71c3e0ab80918a25c176ead378015e863 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 2549cc0decd535288c6ea0a41e506d453be076ed..fd465bbd6497dc328e1ac32e6f8c02617e9e8061 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 680c7d77d9d4ee1069b0db88b60947e3e13690f5..18eea9e8b2cb9efa197bda19ebd294eb75e5ee43 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 7713024853a3774d725dcd8570be6ea95777b1bd..fc2380eafd19896d338b79da0a4a601d9f6bd2ad 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 2f0f3fcfc8e59bfa997a72ae3646fe9611c42898..85344026990854daa9dd325b2327cbcd6f4966c5 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 d4741c2116a0cc5481ecd63eb93658208a5f114f..66605b0d188a345737e204b383dc11dc04d1b4e8 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 4cd8f7ca47b496d09971d991b966b0df6eb5edf5..1b553acccd3e9a6fb87d12b1fc7ffe747d74d807 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 620afee43f7af93afba229850cb4333fd8c88514..925a746f5e1b5d144d3e93733893694e2e8f83b9 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 beda5f49e0e54248a91872c0f51581e703cd585c..ab0daec58b18c514b18e9e3f5c32dea4c3e99cee 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 6fc0af6baa6ba1282f85b2cdeac05c93d0d8e98f..c8b96eb3a05a5423c430e8de6a94dc03b3dc8e20 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 d920a7d2a93ae9b8f5277142137d616bcbf17fd5..30590962809765791957145f87454717e15771f2 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 8c9f215563c79c6982a618994913c253907d3e2d..893f70ae913e5d534b5dac473a81aa77eb529b4e 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 c0db77cfa772407b297da3c8a63468d50cbd99c6..822223da2bddb59138a3d18a20c0b748ddd512aa 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 57e1e108a96160bb2a7ff1b3c6d2558b0c5e807e..82ec0d17b1403b722f2bc784c803f220917896a7 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 150710d303db747ace46c3944c126fdecad3816d..706012283b147e4e99d0e19bbeb0388c61784aec 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 360c9672b2890f34c61a62131a22eda9cc0e1061..cebbcef5dbf6b7e35a932f3baa649e9e9b23614f 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 4ef123dcf5af20aa4e3947cb4d3728a7f96b0319..ebe28593443a459ea0891c366430defb136159e6 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 0bfaa42a954798e3e3c78828964d4f5e563e9532..c124981f5745b777bdd89e4dc59afe69b56243b5 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 45da5647a116ca05317862376546c22c8824f7f5..01e52295213fd30e28d0d6637fefee7724b02cc5 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 4bb4ab17cad169854346fd41e54356cee8ff7d8a..4d2212e5eb7d9a971154fe9cbb9ac2cbc9521be7 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 23637fd5c25e8708dc00cd7f0030256b1444b407..ee81c610f2c244f007b60ab70845885896c12cb7 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 742c8c95be15520ebb6fd59c6be86f7335d855c0..113f50ea29cd06b243d043a81285797cd04df4fa 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 5edf38b704ce896cc65a10921e86c581d068f94a..e2489c01022b1ce301ab0a9a2472250c88547b74 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".