From f84f9ea8d57692715a108b315befdce2bcb3a678 Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Tue, 29 Aug 2023 15:06:33 -0700 Subject: [PATCH] fixing build broken by changed dependency --- coq/extracted/Extract.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/extracted/Extract.v b/coq/extracted/Extract.v index 4d9109b33..cc2c9b39d 100644 --- a/coq/extracted/Extract.v +++ b/coq/extracted/Extract.v @@ -31,6 +31,6 @@ Extract Constant ClassicalDedekindReals.sig_not_dec => false. (* Ugh *) (* Set Extraction AccessOpaque. *) -Extraction Library Vector. +(* Extraction Library Vector. *) Recursive Extraction Library MorelloCapsGS. Recursive Extraction Library CheriMemory.