From f8a2fb5187c295aff10970d91d1781ce38005f48 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 16 Apr 2024 00:29:03 -0400 Subject: [PATCH] directly Require Vector in Lib.Core --- src/Rupicola/Lib/Core.v | 1 + 1 file changed, 1 insertion(+) 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