diff options
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 e6bcefe22..94f6f52cb 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] *) |