diff --git a/theories/typing/base.v b/theories/typing/base.v
index f5cb2484832362f36f4696b9dacc0510c2c8258b..3ccbee1fc01fcf598cacb107645605c8ee40ed7b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,5 +1,4 @@
 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. *)