diff --git a/_CoqProject b/_CoqProject
index e334a62dafc1d78ef582863c5ba2cec9bfbaef1f..5cd928c73d0464b51d3dcf3c7f1e4e0b45412e4e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,6 +24,7 @@ theories/lang/proofmode.v
 theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/spawn.v
+theories/typing/base.v
 theories/typing/type.v
 theories/typing/util.v
 theories/typing/lft_contexts.v
diff --git a/theories/typing/base.v b/theories/typing/base.v
new file mode 100644
index 0000000000000000000000000000000000000000..913b772e6d3387f3695019dae64d4574e44a815d
--- /dev/null
+++ b/theories/typing/base.v
@@ -0,0 +1,14 @@
+From lrust.lifetime Require Export frac_borrow.
+
+Create HintDb lrust_typing.
+Create HintDb lrust_typing_merge.
+
+(* We first try to solve everything without the merging rules, and
+   then start from scratch with them.
+
+   The reason is that we want we want the search proof search for
+   [tctx_extract_hasty] to suceed even if the type is an evar, and
+   merging makes it diverge in this case. *)
+Ltac solve_typing :=
+  (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
+  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 9ee1956b82c9f16dd453f4d91a7a73a1cfaeb6d2..dce104cb3562bc7400b1acbc266245e7bedc0375 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
 From lrust.lang Require Import proofmode.
+From lrust.typing Require Export base.
 From lrust.lifetime Require Import frac_borrow.
 Set Default Proof Using "Type".
 
@@ -453,19 +454,6 @@ End elctx_incl.
 
 Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 
-Create HintDb lrust_typing.
-Create HintDb lrust_typing_merge.
-
-(* We first try to solve everything without the merging rules, and
-   then start from scratch with them.
-
-   The reason is that we want we want the search proof search for
-   [tctx_extract_hasty] to suceed even if the type is an evar, and
-   merging makes it diverge in this case. *)
-Ltac solve_typing :=
-  (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
-  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 706f7b2c1be6c05fe329974211894a5b6addc157..94219da468cbd76c1bc4984c64c4d18e5308c181 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -2,6 +2,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Export frac_borrow.
+From lrust.typing Require Export base.
 From lrust.typing Require Import lft_contexts.
 Set Default Proof Using "Type".