Merge branch 'v8.5'

6 files changed, 23 insertions, 28 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 697f482c49..23320daefb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -395,7 +395,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
 	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0f3ea1d0a6..d4b3812645 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -351,12 +351,20 @@ let translate_module env mp inl = function
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
     finalize_module env mp t restype
 
-let rec translate_mse_incl env mp inl = function
+let rec translate_mse_inclmod env mp inl = function
   |MEident mp1 ->
     let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr mb.mod_type in
     sign,None,mb.mod_delta,Univ.ContextSet.empty
   |MEapply (fe,arg) ->
-    let ftrans = translate_mse_incl env mp inl fe in
+    let ftrans = translate_mse_inclmod 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 *)
+
+let translate_mse_incl is_mod env mp inl me =
+  if is_mod then
+    translate_mse_inclmod env mp inl me
+  else
+    let mtb = translate_modtype env mp inl ([],me) in
+    let sign = clean_bounded_mod_expr mtb.mod_type in
+    sign,None,mtb.mod_delta,mtb.mod_constraints
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 80db12b0d3..bc0e20205a 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -36,11 +36,14 @@ val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
-val translate_mse_incl :
-  env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
-
 val finalize_module :
   env -> module_path -> module_expression translation ->
   (module_type_entry * inline) option ->
   module_body
+
+(** [translate_mse_incl] translate the mse of a module or
+    module type given to an Include *)
+
+val translate_mse_incl :
+  bool -> 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..ec245b0648 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,13 +682,8 @@ let end_modtype l senv =
 let add_include me is_module inl senv =
   let open Mod_typing in
   let mp_sup = senv.modpath in
-  let sign,cst,resolver =
-    if is_module then
-      let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
-      sign,cst,reso
-    else
-      let mtb = translate_modtype senv.env mp_sup inl ([],me) in
-      mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
+  let sign,_,resolver,cst =
+    translate_mse_incl is_module senv.env mp_sup inl me
   in
   let senv = add_constraints (Now (false, cst)) senv in
   (* Include Self support  *)
@@ -706,17 +701,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) =