diff options
Diffstat (limited to 'contrib/extraction/miniml.mli')
| -rw-r--r-- | contrib/extraction/miniml.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 1cbfe3a55f..7dd1316c93 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -61,8 +61,8 @@ type ml_decl = type extraction_params = { lang : string; - modular : bool; - module_name : string; + toplevel : bool; + mod_name : string option; to_appear : global_reference list } module type Mlpp_param = sig |