From a17891fdc314d0fe5246ab785268e2005a8c98b2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 Dec 2015 18:33:14 +0100
Subject: spawn: fix leak of file descriptors

The interesting manifestation of the bug was Unix.select
returning no error but the empty list of descriptors, as if
a timeout did happen.
---
 lib/spawn.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/spawn.ml b/lib/spawn.ml
index 851c6a2235..01f6a4f8d3 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
 
-- 
cgit v1.2.3


From 840cefca77a48ad68641539cd26d8d2e8c9dc031 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 17 Dec 2015 20:32:09 +0100
Subject: (Partial) fix for bug #4453: raise an error instead of an anomaly.

---
 pretyping/typing.ml           | 18 +++++++++++++++---
 test-suite/bugs/closed/4453.v |  8 ++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/4453.v

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb5927dbf7..db980e455a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -144,8 +144,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. *)
@@ -264,6 +269,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)
@@ -271,12 +277,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
@@ -285,6 +294,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
@@ -292,6 +302,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
@@ -301,6 +312,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/4453.v b/test-suite/bugs/closed/4453.v
new file mode 100644
index 0000000000..009dd5e3ca
--- /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.
-- 
cgit v1.2.3


From 5122a39888cfc6afd2383d59465324dd67b69f4a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 21 Dec 2015 18:56:43 +0100
Subject: Inclusion of functors with restricted signature is now forbidden (fix
 #3746)

 The previous behavior was to include the interface of such a functor,
 possibly leading to the creation of unexpected axioms, see bug report #3746.
 In the case of non-functor module with restricted signature, we could
 simply refer to the original objects (strengthening), but for a functor,
 the inner objects have no existence yet. As said in the new error message,
 a simple workaround is hence to first instantiate the functor, then include
 the local instance:

  Module LocalInstance := Funct(Args).
  Include LocalInstance.

 By the way, the mod_type_alg field is now filled more systematically,
 cf new comments in declarations.mli. This way, we could use it to know
 whether a module had been given a restricted signature (via ":"). Earlier,
 some mod_type_alg were None in situations not handled by the extraction
 (MEapply of module type).

 Some code refactoring on the fly.
---
 kernel/declarations.mli           |  23 ++++---
 kernel/mod_typing.ml              | 128 +++++++++++++++++++++-----------------
 kernel/mod_typing.mli             |  24 ++++---
 kernel/modops.ml                  |   7 ++-
 kernel/modops.mli                 |   5 +-
 kernel/safe_typing.ml             |   2 +-
 plugins/extraction/extract_env.ml |  17 ++---
 test-suite/bugs/closed/3746.v     |  92 +++++++++++++++++++++++++++
 toplevel/himsg.ml                 |   7 +++
 9 files changed, 220 insertions(+), 85 deletions(-)
 create mode 100644 test-suite/bugs/closed/3746.v

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75b..0b8272b43d 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 bd7ee7b339..8a1634881f 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 bc0e20205a..d07d59dd9b 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 cbb7963315..341c3993a3 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 a335ad9b4a..86aae598c2 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 e0a07dcc3a..036555309f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -746,7 +746,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/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7014df83fd..9964280336 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/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v
new file mode 100644
index 0000000000..a9463f94bb
--- /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/toplevel/himsg.ml b/toplevel/himsg.ml
index 8f380830db..a3d502dce4 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -924,6 +924,12 @@ let explain_label_missing l s =
   str "The field " ++ str (Label.to_string 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 *)
 
-- 
cgit v1.2.3


From b2eaecf0e748e3c286e1ef337f72cee6d3475162 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Dec 2015 02:48:45 +0100
Subject: Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.

The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
---
 pretyping/evd.ml              | 7 ++++++-
 test-suite/bugs/closed/4462.v | 7 +++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4462.v

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c9b9f34414..8edc7a17c6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -658,7 +658,12 @@ let add d e i = match i.evar_body with
 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/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v
new file mode 100644
index 0000000000..c680518c6a
--- /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).
-- 
cgit v1.2.3


From d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 31 Dec 2015 17:00:42 +0100
Subject: Do not dump a glob reference when its location is ghost. (Fix bug
 #4469)

This patch also causes the code to finish a bit faster in the NoGlob case
by not preparing a string for dump_string. It also optimizes
Dumpglob.is_ghost by only checking whether the end position is zero.

Note that no ghost locations were part of the glob files of the standard
library before the patch. Note also that the html documentation of the
standard library is bitwise identical before and after the patch.
---
 interp/dumpglob.ml | 7 +++++--
 lib/loc.ml         | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c18ceecaba..c7d3da653c 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/lib/loc.ml b/lib/loc.ml
index b62677d484..9043bee075 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
-- 
cgit v1.2.3