diff --git a/theories/typing/type.v b/theories/typing/type.v
index 7672f3cf7380e90ee698b355667ffac2e8ce1920..0e2ed5ec73e730927a53887160bb31a5d2ae998c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,6 +1,6 @@
 From gpfsl.lang Require Export notation.
 From gpfsl.base_logic Require Export na.
-From gpfsl.logic Require Export na_invariants view_invariants.
+From gpfsl.logic Require Export na_invariants.
 From lrust.lifetime Require Export frac_borrow.
 From lrust.typing Require Export base.
 From lrust.typing Require Import lft_contexts.