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.