diff options
| author | Pierre Letouzey | 2014-05-23 17:19:59 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2015-01-11 09:49:32 +0100 |
| commit | d103a645df233dd40064e968fa8693607defa6a7 (patch) | |
| tree | 34851e9f2db6029d83b5da3eb0d911082078e39d /plugins/extraction/modutil.ml | |
| parent | e135bbb71b0e496c016aa89701bd4050cba49f5e (diff) | |
Extraction: discard unnecessary code inside modules without signatures
In the case of an inner module without explicit signature,
(and not used later in a functor application), we now extract
only the needed items (used later or asked by the user),
instead of blindly extracting all fields as earlier.
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index e6bcefe22b..94f6f52cbe 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -197,6 +197,11 @@ let rec msig_of_ms = function let signature_of_structure s = List.map (fun (mp,ms) -> mp,msig_of_ms ms) s +let rec mtyp_of_mexpr = function + | MEfunctor (id,ty,e) -> MTfunsig (id,ty, mtyp_of_mexpr e) + | MEstruct (mp,str) -> MTsig (mp, msig_of_ms str) + | _ -> assert false + (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) |