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.

6 files changed, 6 insertions, 18 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) =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8efc36df7..8f380830d 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 *)