diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index c4dce1c7b..126305566 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -487,6 +487,10 @@ let init modular library = reset (); if modular && lang () = Scheme then error_scheme () +let warns () = + warning_opaques (access_opaque ()); + warning_axioms () + (* From a list of [reference], let's retrieve whether they correspond to modules or [global_reference]. Warn the user if both is possible. *) @@ -513,8 +517,7 @@ let full_extr f (refs,mps) = init false false; List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps; let struc = optimize_struct (refs,mps) (mono_environment refs mps) in - warning_opaques (); - warning_axioms (); + warns (); print_structure_to_file (mono_filename f) false struc; reset () @@ -527,8 +530,7 @@ let separate_extraction lr = init true false; let refs,mps = locate_ref lr in let struc = optimize_struct (refs,mps) (mono_environment refs mps) in - warning_opaques (); - warning_axioms (); + warns (); let print = function | (MPfile dir as mp, sel) as e -> print_structure_to_file (module_filename mp) false [e] @@ -546,8 +548,7 @@ let simple_extraction r = match locate_ref [r] with init false false; let struc = optimize_struct ([r],[]) (mono_environment [r] []) in let d = get_decl_in_structure r struc in - warning_opaques (); - warning_axioms (); + warns (); if is_custom r then msgnl (str "(** User defined extraction *)"); print_one_decl struc (modpath_of_r r) d; reset () @@ -573,8 +574,7 @@ let extraction_library is_rec m = in let struc = List.fold_left select [] l in let struc = optimize_struct ([],[]) struc in - warning_opaques (); - warning_axioms (); + warns (); let print = function | (MPfile dir as mp, sel) as e -> let dry = not is_rec && dir <> dir_m in |