aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-10-25 12:14:12 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-10-25 12:14:12 +0100
commitc2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (patch)
treecfabd3b72d81389cf4a7a93cb656534a570ca6ef /kernel
parent1b029b2163386f20179a61f6bdb68e5532f4c306 (diff)
Minor module cleanup : error HigherOrderInclude was never happening
When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/mod_typing.ml2
-rw-r--r--kernel/mod_typing.mli3
-rw-r--r--kernel/modops.ml4
-rw-r--r--kernel/modops.mli3
-rw-r--r--kernel/safe_typing.ml8
5 files changed, 6 insertions, 14 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 922652287..eef83ce74 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 80db12b0d..0c3fb2ba7 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 8733ca8c2..f0cb65c96 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 6fbcd81d0..a335ad9b4 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 9329b1686..fdacbb365 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) =