diff options
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 8 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
6 files changed, 29 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index e4b1af8fe..4e930a09e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -49,6 +49,10 @@ let universes env = env.env_universes let named_context env = env.env_named_context let rel_context env = env.env_rel_context +let empty_context env = + env.env_rel_context = empty_rel_context + && env.env_named_context = empty_named_context + (* Rel context *) let lookup_rel n env = Sign.lookup_rel n env.env_rel_context diff --git a/kernel/environ.mli b/kernel/environ.mli index 2b2be6b6b..baf1a71e1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -35,6 +35,9 @@ val universes : env -> Univ.universes val rel_context : env -> rel_context val named_context : env -> named_context +(* is the local context empty *) +val empty_context : env -> bool + (***********************************************************************) (*s Context of de Bruijn variables (rel_context) *) val push_rel : rel_declaration -> env -> env diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 785e8ebdd..7417b4261 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -136,10 +136,18 @@ and translate_entry_list env msid is_definition sig_e = match e with | SPEconst ce -> let cb = translate_constant env ce in - add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb) + begin match cb.const_hyps with + | (_::_) -> error_local_context (Some l) + | [] -> + add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb) + end | SPEmind mie -> let mib = translate_mind env mie in - add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib) + begin match mib.mind_hyps with + | (_::_) -> error_local_context (Some l) + | [] -> + add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib) + end | SPEmodule me -> let mb = translate_module env is_definition me in let mspec = diff --git a/kernel/modops.ml b/kernel/modops.ml index cd8cbe1ee..ec25459a9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -66,6 +66,14 @@ let error_not_a_constant l = let error_with_incorrect l = error ("Incorrect constraint for label \""^(string_of_label l)^"\"") +let error_local_context lo = + match lo with + None -> + error ("The local context is not empty.") + | (Some l) -> + error ("The local context of the component "^ + (string_of_label l)^" is not empty") + let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb diff --git a/kernel/modops.mli b/kernel/modops.mli index e865159c5..aaff57223 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -90,3 +90,5 @@ val error_not_a_module : string -> 'a val error_not_a_constant : label -> 'a val error_with_incorrect : label -> 'a + +val error_local_context : label option -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 52fe3a135..e200e7bf3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -272,6 +272,7 @@ let end_module l senv = | STRUCT(params,restype) -> (params,restype) in if l <> modinfo.label then error_incompatible_labels l modinfo.label; + if not (empty_context senv.env) then error_local_context None; let functorize_type = List.fold_right (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb)) @@ -366,6 +367,7 @@ let end_modtype l senv = | SIG 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; let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in let mtb = List.fold_right |