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.

1 files changed, 2 insertions, 6 deletions

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) =