diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/modops.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
4 files changed, 10 insertions, 17 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index b20e7259d5..166b230077 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -41,7 +41,7 @@ let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") -let error_result_must_be_signature mtb = +let error_result_must_be_signature () = error "The result module type must be a signature" let error_signature_expected mtb = diff --git a/kernel/modops.mli b/kernel/modops.mli index f102a5b2c0..b8f1f66a3c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -74,7 +74,7 @@ val error_incompatible_labels : label -> label -> 'a val error_no_such_label : label -> 'a -val error_result_must_be_signature : module_type_body -> 'a +val error_result_must_be_signature : unit -> 'a val error_signature_expected : module_type_body -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9b638427cb..ca1bf6f65a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -30,7 +30,6 @@ type modvariant = | NONE | SIG of (* funsig params *) (mod_bound_id * module_type_body) list | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list - * (* optional result type *) module_type_body option | LIBRARY of dir_path type module_info = @@ -224,7 +223,7 @@ let add_module l me senv = (* Interactive modules *) -let start_module l params result senv = +let start_module l params senv = check_label l senv.labset; let rec trans_params env = function | [] -> env,[] @@ -237,20 +236,13 @@ let start_module l params result senv = env, (mbid,mtb)::transrest in let env,params_body = trans_params senv.env params in - let check_sig mtb = match scrape_modtype env mtb with - | MTBsig _ -> () - | MTBfunsig _ -> error_result_must_be_signature mtb - | _ -> anomaly "start_module: modtype not scraped" - in - let result_body = option_app (translate_modtype env) result in - ignore (option_app check_sig result_body); let msid = make_msid senv.modinfo.seed (string_of_label l) in let mp = MPself msid in let modinfo = { msid = msid; modpath = mp; seed = senv.modinfo.seed; label = l; - variant = STRUCT(params_body,result_body) } + variant = STRUCT params_body } in mp, { old = senv; env = env; @@ -263,13 +255,14 @@ let start_module l params result senv = -let end_module l senv = +let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in - let params, restype = + let restype = option_app (translate_modtype senv.env) restype in + let params = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () - | STRUCT(params,restype) -> (params,restype) + | STRUCT params -> params in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5412287ee4..43755b9085 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,11 +73,11 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : label -> (mod_bound_id * module_type_entry) list - -> module_type_entry option -> safe_environment -> module_path * safe_environment val end_module : - label -> safe_environment -> module_path * safe_environment + label -> module_type_entry option + -> safe_environment -> module_path * safe_environment val start_modtype : |