Merge PR #9525: Remove global output_native_objects flag.

Reviewed-by: ejgallego
Reviewed-by: maximedenes

6 files changed, 12 insertions, 9 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8699583cdf..5fd11e187a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -928,10 +928,10 @@ let append_end_library_hook f =
   let old_f = !end_library_hook in
   end_library_hook := fun () -> old_f(); f ()
 
-let end_library ?except dir =
+let end_library ?except ~output_native_objects dir =
   !end_library_hook();
   let oname = Lib.end_compilation_checks dir in
-  let mp,cenv,ast = Global.export ?except dir in
+  let mp,cenv,ast = Global.export ?except ~output_native_objects dir in
   let prefix, lib_stack = Lib.end_compilation oname in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 7aa4bc30ce..2b28ba908e 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols
 val start_library : library_name -> unit
 
 val end_library :
-  ?except:Future.UUIDSet.t -> library_name ->
+  ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
 (** append a function to be executed at end_library *)
diff --git a/library/global.ml b/library/global.ml
index 784a02449c..cf996ce644 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -143,7 +143,8 @@ let mind_of_delta_kn kn =
 (** Operations on libraries *)
 
 let start_library dir = globalize (Safe_typing.start_library dir)
-let export ?except s = Safe_typing.export ?except (safe_env ()) s
+let export ?except ~output_native_objects s =
+  Safe_typing.export ?except ~output_native_objects (safe_env ()) s
 let import c u d = globalize (Safe_typing.import c u d)
 
 
diff --git a/library/global.mli b/library/global.mli
index df18625a5f..4e2ad92717 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> ModPath.t
-val export : ?except:Future.UUIDSet.t -> DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
   ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
diff --git a/library/library.ml b/library/library.ml
index 9b9bd07c93..37dadadb76 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -657,7 +657,7 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo dir f otab =
+let save_library_to ?todo ~output_native_objects dir f otab =
   let except = match todo with
     | None ->
         (* XXX *)
@@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab =
         assert(Filename.check_suffix f ".vio");
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
-  let cenv, seg, ast = Declaremods.end_library ~except dir in
+  let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
   let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
   let tasks, utab, dtab =
     match todo with
@@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if !Flags.output_native_objects then
+    if output_native_objects then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
 	user_err Pp.(str "Could not compile the library to native code.")
diff --git a/library/library.mli b/library/library.mli
index c016352808..a976be0184 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid list -> unit
 
-(** End the compilation of a library and save it to a ".vo" file *)
+(** End the compilation of a library and save it to a ".vo" file.
+    [output_native_objects]: when producing vo objects, also compile the native-code version. *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+  output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :