diff options
| -rw-r--r-- | kernel/mod_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 3 | ||||
| -rw-r--r-- | kernel/modops.ml | 4 | ||||
| -rw-r--r-- | kernel/modops.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 8 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
6 files changed, 6 insertions, 18 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 922652287b..eef83ce743 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -359,4 +359,4 @@ let rec translate_mse_incl env mp inl = function |MEapply (fe,arg) -> let ftrans = translate_mse_incl env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) - |_ -> Modops.error_higher_order_include () + |MEwith _ -> assert false (* No 'with' syntax for modules *) diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 80db12b0d3..0c3fb2ba79 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,6 +36,9 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** [translate_mse_incl] translate the mse of a real module (no + module type here) given to an Include *) + val translate_mse_incl : env -> module_path -> inline -> module_struct_entry -> module_alg_expr translation diff --git a/kernel/modops.ml b/kernel/modops.ml index 8733ca8c2f..f0cb65c967 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,7 +67,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -113,9 +112,6 @@ let error_generative_module_expected l = let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) -let error_higher_order_include () = - raise (ModuleTypingError HigherOrderInclude) - (** {6 Operations on functors } *) let is_functor = function diff --git a/kernel/modops.mli b/kernel/modops.mli index 6fbcd81d03..a335ad9b4a 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -126,7 +126,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -153,5 +152,3 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a - -val error_higher_order_include : unit -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9329b16861..fdacbb365c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -706,17 +706,13 @@ let add_include me is_module inl senv = let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in compute_sign (Modops.subst_signature subst str) mb resolver senv - | str -> resolver,str,senv + | NoFunctor str -> resolver,str,senv in - let resolver,sign,senv = + let resolver,str,senv = let struc = NoFunctor (List.rev senv.revstruct) in let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in compute_sign sign mtb resolver senv in - let str = match sign with - | NoFunctor struc -> struc - | MoreFunctor _ -> Modops.error_higher_order_include () - in let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv in let add senv ((l,elem) as field) = diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8efc36df72..8f380830db 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -924,9 +924,6 @@ let explain_label_missing l s = str "The field " ++ str (Label.to_string l) ++ str " is missing in " ++ str s ++ str "." -let explain_higher_order_include () = - str "You cannot Include a higher-order structure." - let explain_module_error = function | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l @@ -943,7 +940,6 @@ let explain_module_error = function | IncorrectWithConstraint l -> explain_incorrect_label_constraint l | GenerativeModuleExpected l -> explain_generative_module_expected l | LabelMissing (l,s) -> explain_label_missing l s - | HigherOrderInclude -> explain_higher_order_include () (* Module internalization errors *) |