diff --git a/extraction/extraction.v b/extraction/extraction.v index c01426e6a..b4ee50549 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -27,6 +27,8 @@ Require Initializers. (* Standard lib *) From Coq Require Import ExtrOcamlBasic ExtrOcamlNativeString. +Set Extraction OldCoqPrefix. (* TODO: handle when requiring Rocq >= 9.4 *) + (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".