diff --git a/theories/typing/base.v b/theories/typing/base.v
index 796d22432f973267b4883b6c22e4bcb0df81df20..cd2a0b9b9d909100a9bdfd765314fffd70837145 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -3,7 +3,7 @@ From gpfsl.base_logic Require Import na.
 
 (* Last, so that we make sure we shadow the definition of delete for
    sets coming from the prelude. *)
-From lrust.lang.lib Require Export new_delete.
+From lrust.lang Require Export new_delete.
 
 Open Scope Z_scope.