diff --git a/src/Rupicola/Lib/Core.v b/src/Rupicola/Lib/Core.v
index 6962e170..5af920ae 100644
--- a/src/Rupicola/Lib/Core.v
+++ b/src/Rupicola/Lib/Core.v
@@ -1,6 +1,7 @@
 From Coq Require Export
      Classes.Morphisms Numbers.DecimalString
      String List ZArith Lia.
+From Coq Require Vector.
 From bedrock2 Require Export
      Array ArrayCasts Map.Separation ProgramLogic
      Map.SeparationLogic Scalars Syntax WeakestPreconditionProperties