directly Require Vector in Lib.Core

mit-plv · Apr 16, 2024 · f8a2fb5 · f8a2fb5
1 parent 6c63c08
commit f8a2fb5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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