Merge branch 'v8.5' into trunk

16 files changed, 268 insertions, 94 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6651ff5f6..d91b90caa 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -462,7 +462,12 @@ let new_evar evd ?naming evi =
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  { d with undf_evars; defn_evars; }
+  let principal_future_goal = match d.principal_future_goal with
+  | None -> None
+  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
+  in
+  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals }
 
 let find d e =
   try EvMap.find e d.undf_evars
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c18ceecab..c7d3da653 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -139,12 +139,15 @@ let interval loc =
   loc1, loc2-1
 
 let dump_ref loc filepath modpath ident ty =
-  if !glob_output = Feedback then
+  match !glob_output with
+  | Feedback ->
     Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
-  else
+  | NoGlob -> ()
+  | _ when not (Loc.is_ghost loc) ->
     let bl,el = interval loc in
     dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 		  bl el filepath modpath ident ty)
+  | _ -> ()
 
 let dump_reference loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75..0b8272b43 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -238,17 +238,26 @@ and module_body =
   { mod_mp : module_path; (** absolute path of the module *)
     mod_expr : module_implementation; (** implementation *)
     mod_type : module_signature; (** expanded type *)
-    (** algebraic type, kept if it's relevant for extraction *)
-    mod_type_alg : module_expression option;
-    (** set of all universes constraints in the module  *)
-    mod_constraints : Univ.ContextSet.t;
-    (** quotiented set of equivalent constants and inductive names *)
-    mod_delta : Mod_subst.delta_resolver;
+    mod_type_alg : module_expression option; (** algebraic type *)
+    mod_constraints : Univ.ContextSet.t; (**
+      set of all universes constraints in the module  *)
+    mod_delta : Mod_subst.delta_resolver; (**
+      quotiented set of equivalent constants and inductive names *)
     mod_retroknowledge : Retroknowledge.action list }
 
+(** For a module, there are five possible situations:
+    - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
+    - [Module M := E] then [mod_expr = Algebraic E; mod_type_alg = None]
+    - [Module M : T := E] then [mod_expr = Algebraic E; mod_type_alg = Some T]
+    - [Module M. ... End M] then [mod_expr = FullStruct; mod_type_alg = None]
+    - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
+    And of course, all these situations may be functors or not. *)
+
 (** A [module_type_body] is just a [module_body] with no
     implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge] *)
+    an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+    the algebraic definition of this module type, or [None]
+    if it has been built interactively. *)
 
 and module_type_body = module_body
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3c58e788c..3a75a74d9 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
 open Mod_subst
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 let rec mp_from_mexpr = function
   | MEident mp -> mp
@@ -183,8 +183,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
 	  begin
             try
               let mtb_old = module_type_of_module old in
-              Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
-	    with Failure _ -> error_incorrect_with_constraint lab
+              let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+              Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+	    with Failure _ ->
+              (* TODO: where can a Failure come from ??? *)
+              error_incorrect_with_constraint lab
 	  end
 	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
@@ -238,104 +241,89 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
-
 let check_with env mp (sign,alg,reso,cst) = function
   |WithDef(idl,c) ->
     let struc = destr_nofunctor sign in
     let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
-    let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
-    (NoFunctor struc'),alg',reso, cst+++cst'
+    let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
+    NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
-    let alg' = mk_alg_with alg wd in
-    (NoFunctor struc'),alg',reso', cst+++cst'
+    NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
 
-let mk_alg_app mpo alg arg = match mpo, alg with
-  | Some _, Some alg -> Some (MEapply (alg,arg))
-  | _ -> None
+let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
+  let farg_id, farg_b, fbody_b = destr_functor sign in
+  let mtb = module_type_of_module (lookup_module mp1 env) in
+  let cst2 = Subtyping.check_subtypes env mtb farg_b in
+  let mp_delta = discr_resolver mtb in
+  let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+  let subst = map_mbid farg_id mp1 mp_delta in
+  let body = subst_signature subst fbody_b in
+  let alg' = mkalg alg mp1 in
+  let reso' = subst_codom_delta_resolver subst reso in
+  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
 
 (** Translation of a module struct entry :
     - We translate to a module when a [module_path] is given,
       otherwise to a module type.
     - The first output is the expanded signature
     - The second output is the algebraic expression, kept for the extraction.
-      It is never None when translating to a module, but for module type
-      it could not be contain [SEBapply] or [SEBfunctor].
 *)
 
+let mk_alg_app alg arg = MEapply (alg,arg)
+
 let rec translate_mse env mpo inl = function
-  |MEident mp1 ->
-    let sign,reso = match mpo with
-      |Some mp ->
-        let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
-        mb.mod_type, mb.mod_delta
-      |None ->
-        let mtb = lookup_modtype mp1 env in
-        mtb.mod_type, mtb.mod_delta
+  |MEident mp1 as me ->
+    let mb = match mpo with
+      |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
+      |None -> lookup_modtype mp1 env
     in
-    sign,Some (MEident mp1),reso,Univ.ContextSet.empty
+    mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
-    translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+    translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
   |MEwith(me, with_decl) ->
     assert (mpo == None); (* No 'with' syntax for modules *)
     let mp = mp_from_mexpr me in
     check_with env mp (translate_mse env None inl me) with_decl
 
-and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
-  let farg_id, farg_b, fbody_b = destr_functor sign in
-  let mtb = module_type_of_module (lookup_module mp1 env) in
-  let cst2 = Subtyping.check_subtypes env mtb farg_b in
-  let mp_delta = discr_resolver mtb in
-  let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
-  let subst = map_mbid farg_id mp1 mp_delta in
-  let body = subst_signature subst fbody_b in
-  let alg' = mkalg alg mp1 in
-  let reso' = subst_codom_delta_resolver subst reso in
-  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
-
-let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
-  | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
-  | _ -> None
-
-let mk_mod mp e ty ty' cst reso =
+let mk_mod mp e ty cst reso =
   { mod_mp = mp;
     mod_expr = e;
     mod_type = ty;
-    mod_type_alg = ty';
+    mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = reso;
     mod_retroknowledge = [] }
 
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
 
 let rec translate_mse_funct env mpo inl mse = function
   |[] ->
     let sign,alg,reso,cst = translate_mse env mpo inl mse in
-    sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+    sign, NoFunctor alg, reso, cst
   |(mbid, ty) :: params ->
     let mp_id = MPbound mbid in
     let mtb = translate_modtype env mp_id inl ([],ty) in
     let env' = add_module_type mp_id mtb env in
     let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
-    let alg' = mk_alg_funct mpo mbid mtb alg in
+    let alg' = MoreFunctor (mbid,mtb,alg) in
     MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
 
 and translate_modtype env mp inl (params,mte) =
   let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
   let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
   let mtb' = subst_modtype_and_resolver mtb mp in
-  { mtb' with mod_type_alg = alg }
+  { mtb' with mod_type_alg = Some alg }
 
 (** [finalize_module] :
-    from an already-translated (or interactive) implementation
-    and a signature entry, produce a final [module_expr] *)
+    from an already-translated (or interactive) implementation and
+    an (optional) signature entry, produces a final [module_body] *)
 
 let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
   |None ->
     let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
-    mk_mod mp impl sign None cst reso
+    mk_mod mp impl sign cst reso
   |Some (params_mte,inl) ->
     let res_mtb = translate_modtype env mp inl params_mte in
     let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
@@ -344,33 +332,59 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
-      (** cst from module body typing, cst' from subtyping, 
-          and constraints from module type. *)
-      mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+      (** cst from module body typing,
+          cst' from subtyping,
+          constraints from module type. *)
+      mod_constraints =
+        Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
     let mtb = translate_modtype env mp inl (params,ty) in
     module_body_of_type mp mtb
   |MExpr (params,mse,oty) ->
-    let t = translate_mse_funct env (Some mp) inl mse params in
+    let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
-    finalize_module env mp t restype
+    finalize_module env mp (sg,Some alg,reso,cst) restype
+
+(** We now forbid any Include of functors with restricted signatures.
+    Otherwise, we could end with the creation of undesired axioms
+    (see #3746). Note that restricted non-functorized modules are ok,
+    thanks to strengthening. *)
+
+let rec unfunct = function
+  |NoFunctor me -> me
+  |MoreFunctor(_,_,me) -> unfunct me
+
+let rec forbid_incl_signed_functor env = function
+  |MEapply(fe,_) -> forbid_incl_signed_functor env fe
+  |MEwith _ -> assert false (* No 'with' syntax for modules *)
+  |MEident mp1 ->
+    let mb = lookup_module mp1 env in
+    match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
+    |MoreFunctor _, Some _, _ ->
+      (* functor + restricted signature = error *)
+      error_include_restricted_functor mp1
+    |MoreFunctor _, None, Algebraic me ->
+      (* functor, no signature yet, a definition which may be restricted *)
+      forbid_incl_signed_functor env (unfunct me)
+    |_ -> ()
 
 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
+    sign,(),mb.mod_delta,Univ.ContextSet.empty
   |MEapply (fe,arg) ->
     let ftrans = translate_mse_inclmod env mp inl fe in
-    translate_apply env inl ftrans arg (fun _ _ -> None)
+    translate_apply env inl ftrans arg (fun _ _ -> ())
   |MEwith _ -> assert false (* No 'with' syntax for modules *)
 
 let translate_mse_incl is_mod env mp inl me =
   if is_mod then
+    let () = forbid_incl_signed_functor env me in
     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
+    sign,(),mtb.mod_delta,mtb.mod_constraints
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index bc0e20205..d07d59dd9 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -14,9 +14,18 @@ open Names
 
 (** Main functions for translating module entries *)
 
+(** [translate_module] produces a [module_body] out of a [module_entry].
+    In the output fields:
+    - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
+    - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.
+*)
+
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
+(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
+    cannot be [None] (and of course [mod_expr] is [Abstract]). *)
+
 val translate_modtype :
   env -> module_path -> inline -> module_type_entry -> module_type_body
 
@@ -24,20 +33,21 @@ val translate_modtype :
     - We translate to a module when a [module_path] is given,
       otherwise to a module type.
     - The first output is the expanded signature
-    - The second output is the algebraic expression, kept for the extraction.
-      It is never None when translating to a module, but for module type
-      it could not be contain applications or functors.
-*)
+    - The second output is the algebraic expression, kept mostly for
+      the extraction. *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
+(** From an already-translated (or interactive) implementation and
+    an (optional) signature entry, produces a final [module_body] *)
+
 val finalize_module :
-  env -> module_path -> module_expression translation ->
+  env -> module_path -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
   module_body
 
@@ -46,4 +56,4 @@ val finalize_module :
 
 val translate_mse_incl :
   bool -> env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
+    unit translation
diff --git a/kernel/modops.ml b/kernel/modops.ml
index cbb796331..341c3993a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,15 +67,13 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
+  | IncludeRestrictedFunctor of module_path
 
 exception ModuleTypingError of module_typing_error
 
 let error_existing_label l =
   raise (ModuleTypingError (LabelAlreadyDeclared l))
 
-let error_application_to_not_path mexpr =
-  raise (ModuleTypingError (ApplicationToNotPath mexpr))
-
 let error_not_a_functor () =
   raise (ModuleTypingError NotAFunctor)
 
@@ -112,6 +110,9 @@ let error_generative_module_expected l =
 let error_no_such_label_sub l l1 =
   raise (ModuleTypingError (LabelMissing (l,l1)))
 
+let error_include_restricted_functor mp =
+  raise (ModuleTypingError (IncludeRestrictedFunctor mp))
+
 (** {6 Operations on functors } *)
 
 let is_functor = function
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a335ad9b4..86aae598c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,13 +126,12 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
+  | IncludeRestrictedFunctor of module_path
 
 exception ModuleTypingError of module_typing_error
 
 val error_existing_label : Label.t -> 'a
 
-val error_application_to_not_path : module_struct_entry -> 'a
-
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
@@ -152,3 +151,5 @@ 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_include_restricted_functor : module_path -> 'a
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f86fdfa97..c7ab6491d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -748,7 +748,7 @@ 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,_,resolver,cst =
+  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
diff --git a/lib/loc.ml b/lib/loc.ml
index b62677d48..9043bee07 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -31,7 +31,7 @@ let ghost = {
   fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = 0; ep = 0; }
 
-let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *)
+let is_ghost loc = loc.ep = 0
 
 let merge loc1 loc2 =
   if loc1.bp < loc2.bp then
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 851c6a223..01f6a4f8d 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -175,7 +175,7 @@ let is_alive p = p.alive
 let uid { pid; } = string_of_int pid
 let unixpid { pid; } = pid
 
-let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) =
+let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
   p.alive <- false;
   if not alive then prerr_endline "This process is already dead"
   else begin try
@@ -183,6 +183,8 @@ let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) =
     output_death_sentence (uid p) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
+    close_in_noerr oob_resp;
+    close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
     p.watch <- None
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
@@ -247,13 +249,15 @@ let is_alive p = p.alive
 let uid { pid; } = string_of_int pid
 let unixpid { pid = pid; } = pid
 
-let kill ({ pid = unixpid; oob_req; cin; cout; alive } as p) =
+let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
   p.alive <- false;
   if not alive then prerr_endline "This process is already dead"
   else begin try
     output_death_sentence (uid p) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
+    close_in_noerr oob_resp;
+    close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7014df83f..996428033 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -177,8 +177,7 @@ let factor_fix env l cb msb =
 
 let expand_mexpr env mp me =
   let inl = Some (Flags.get_inline_level()) in
-  let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in
-  sign
+  Mod_typing.translate_mse env (Some mp) inl me
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
@@ -231,10 +230,9 @@ let rec extract_structure_spec env mp reso = function
 
 (* From [module_expression] to specifications *)
 
-(* Invariant: the [me] given to [extract_mexpr_spec] should either come
-   from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
-   This way, any encountered [MEident] should be a true module type.
-*)
+(* Invariant: the [me_alg] given to [extract_mexpr_spec] and
+   [extract_mexpression_spec] should come from a [mod_type_alg] field.
+   This way, any encountered [MEident] should be a true module type. *)
 
 and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
@@ -247,7 +245,9 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
       MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
-  | MEapply _ -> extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+  | MEapply _ ->
+     (* No higher-order module type in OCaml : we use the expanded version *)
+     extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
 
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
@@ -335,7 +335,8 @@ and extract_mexpr env mp = function
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
-      extract_msignature env mp no_delta ~all:true (expand_mexpr env mp me)
+      let sign,_,delta,_ = expand_mexpr env mp me in
+      extract_msignature env mp delta ~all:true sign
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp_all mp; Miniml.MEident mp
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f9803b62..11ad7bfdf 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -143,8 +143,13 @@ let e_judge_of_cast env evdref cj k tj =
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
 
-(* The typing machine without information, without universes but with
-   existential variables. *)
+let enrich_env env evdref =
+  let penv = Environ.pre_env env in
+  let penv' = Pre_env.({ penv with env_stratification =
+    { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
+  Environ.env_of_pre_env penv'
+			  
+(* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
@@ -263,6 +268,7 @@ and execute_recdef env evdref (names,lar,vdef) =
 and execute_array env evdref = Array.map (execute env evdref)
 
 let check env evdref c t =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   if not (Evarconv.e_cumul env evdref j.uj_type t) then
     error_actual_type env j (nf_evar !evdref t)
@@ -270,12 +276,15 @@ let check env evdref c t =
 (* Type of a constr *)
 
 let unsafe_type_of env evd c =
-  let j = execute env (ref evd) c in
+  let evdref = ref evd in
+  let env = enrich_env env evdref in
+  let j = execute env evdref c in
     j.uj_type
 
 (* Sort of a type *)
 
 let sort_of env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   let a = e_type_judgment env evdref j in
   a.utj_type
@@ -284,6 +293,7 @@ let sort_of env evdref c =
 
 let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -291,6 +301,7 @@ let type_of ?(refresh=false) env evd c =
     else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -300,6 +311,7 @@ let e_type_of ?(refresh=false) env evdref c =
     else j.uj_type
 
 let solve_evars env evdref c =
+  let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
   nf_evar !evdref c
diff --git a/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v
new file mode 100644
index 000000000..a9463f94b
--- /dev/null
+++ b/test-suite/bugs/closed/3746.v
@@ -0,0 +1,92 @@
+
+(* Bug report #3746 : Include and restricted signature *)
+
+Module Type MT. Parameter p : nat. End MT.
+Module Type EMPTY. End EMPTY.
+Module Empty. End Empty.
+
+(* Include of an applied functor with restricted sig :
+   Used to create axioms (bug report #3746), now forbidden. *)
+
+Module F (X:EMPTY) : MT.
+ Definition p := 0.
+End F.
+
+Module InclFunctRestr.
+ Fail Include F(Empty).
+End InclFunctRestr.
+
+(* A few variants (indirect restricted signature), also forbidden. *)
+
+Module F1 := F.
+Module F2 (X:EMPTY) := F X.
+
+Module F3a (X:EMPTY). Definition p := 0. End F3a.
+Module F3 (X:EMPTY) : MT := F3a X.
+
+Module InclFunctRestrBis.
+ Fail Include F1(Empty).
+ Fail Include F2(Empty).
+ Fail Include F3(Empty).
+End InclFunctRestrBis.
+
+(* Recommended workaround: manual instance before the include. *)
+
+Module InclWorkaround.
+ Module Temp := F(Empty).
+ Include Temp.
+End InclWorkaround.
+
+Compute InclWorkaround.p.
+Print InclWorkaround.p.
+Print Assumptions InclWorkaround.p. (* Closed under the global context *)
+
+
+
+(* Related situations which are ok, just to check *)
+
+(* A) Include of non-functor with restricted signature :
+   creates a proxy to initial stuff *)
+
+Module M : MT.
+  Definition p := 0.
+End M.
+
+Module InclNonFunct.
+  Include M.
+End InclNonFunct.
+
+Definition check : InclNonFunct.p = M.p := eq_refl.
+Print Assumptions InclNonFunct.p. (* Closed *)
+
+
+(* B) Include of a module type with opaque content:
+   The opaque content is "copy-pasted". *)
+
+Module Type SigOpaque.
+ Definition p : nat. Proof. exact 0. Qed.
+End SigOpaque.
+
+Module InclSigOpaque.
+ Include SigOpaque.
+End InclSigOpaque.
+
+Compute InclSigOpaque.p.
+Print InclSigOpaque.p.
+Print Assumptions InclSigOpaque.p. (* Closed *)
+
+
+(* C) Include of an applied functor with opaque proofs :
+   opaque proof "copy-pasted" (and substituted). *)
+
+Module F' (X:EMPTY).
+ Definition p : nat. Proof. exact 0. Qed.
+End F'.
+
+Module InclFunctOpa.
+ Include F'(Empty).
+End InclFunctOpa.
+
+Compute InclFunctOpa.p.
+Print InclFunctOpa.p.
+Print Assumptions InclFunctOpa.p. (* Closed *)
diff --git a/test-suite/bugs/closed/4453.v b/test-suite/bugs/closed/4453.v
new file mode 100644
index 000000000..009dd5e3c
--- /dev/null
+++ b/test-suite/bugs/closed/4453.v
@@ -0,0 +1,8 @@
+
+Section Foo.
+Variable A : Type.
+Lemma foo : A -> True. now intros _. Qed.
+Goal Type -> True.
+rename A into B.
+intros A.
+Fail apply foo.
diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v
new file mode 100644
index 000000000..c680518c6
--- /dev/null
+++ b/test-suite/bugs/closed/4462.v
@@ -0,0 +1,7 @@
+Variables P Q : Prop.
+Axiom pqrw : P <-> Q.
+
+Require Setoid.
+
+Goal P -> Q.
+unshelve (rewrite pqrw).
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e21b6b41c..3308903dd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -924,6 +924,12 @@ let explain_label_missing l s =
   str "The field " ++ pr_label l ++ str " is missing in "
   ++ str s ++ str "."
 
+let explain_include_restricted_functor mp =
+  let q = Nametab.shortest_qualid_of_module mp in
+  str "Cannot include the functor " ++ Libnames.pr_qualid q ++
+  strbrk " since it has a restricted signature. " ++
+  strbrk "You may name first an instance of this functor, and include it."
+
 let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
   | LabelAlreadyDeclared l -> explain_label_already_declared l
@@ -940,6 +946,7 @@ 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
+  | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp
 
 (* Module internalization errors *)