diff options
Diffstat (limited to 'contrib/extraction/mlutil.mli')
| -rw-r--r-- | contrib/extraction/mlutil.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index b68d4a954a..af931b6486 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -39,10 +39,21 @@ val betared_decl : ml_decl -> ml_decl val uncurrify_ast : ml_ast -> ml_ast val uncurrify_decl : ml_decl -> ml_decl -(*s Table for direct extractions to ML values. *) +(*s Optimization. *) module Refset : Set.S with type elt = global_reference +type extraction_params = { + modular : bool; (* modular extraction *) + no_opt : bool; (* no optimization at all *) + to_keep : Refset.t; (* globals to keep *) + to_expand : Refset.t; (* globals to expand *) +} + +val optimize : extraction_params -> ml_decl list -> ml_decl list + +(*s Table for direct extractions to ML values. *) + val is_ml_extraction : global_reference -> bool val find_ml_extraction : global_reference -> string |