From c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 25 Oct 2015 12:14:12 +0100
Subject: 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.
---
 kernel/safe_typing.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'kernel/safe_typing.ml')

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) =
-- 
cgit v1.2.3