From 7d6d9c5aea6232200b99e828b7e04b49808f8478 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 19 Oct 2015 18:13:32 +0200
Subject: Do occur-check w.r.t existential's types also when instantiating an
 evar.

---
 pretyping/evarsolve.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bbc4f1db29..b384bdfe16 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1272,6 +1272,15 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
           restrict_evar evd evk None (UpdateWith candidates)
       | l -> evd
 
+let occur_evar_upto_types sigma n c =
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
+    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e);
+		occur_rec (existential_type sigma e)
+    | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -1459,7 +1468,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
 	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
 	else t'
   in (!evdref,body)
-
+     
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
  * [define] tries to find an instance lhs such that
@@ -1484,7 +1493,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
-- 
cgit v1.2.3


From a1b828d31c73d3342345243e9fb4af69610616a0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 20 Oct 2015 18:15:04 +0200
Subject: Fix lemma-overloading

Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
---
 pretyping/evarsolve.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b384bdfe16..f06207c3b9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1149,10 +1149,19 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
+let update_evar_source ev1 ev2 evd =
+  let loc, evs2 = evar_source ev2 evd in
+  match evs2 with
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
+     let evi = Evd.find evd ev1 in
+     Evd.add evd ev1 {evi with evar_source = loc, evs2}
+  | _ -> evd
+  
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
+    let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1164,8 +1173,8 @@ let preferred_orientation evd evk1 evk2 =
   let _,src2 = (Evd.find_undefined evd evk2).evar_source in
   (* This is a heuristic useful for program to work *)
   match src1,src2 with
-  | Evar_kinds.QuestionMark _, _ -> true
-  | _,Evar_kinds.QuestionMark _ -> false
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
+  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
-- 
cgit v1.2.3


From ae7e8f8f66359a46e165e1eae6cf15eb09fd66de Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 21 Oct 2015 10:59:36 +0200
Subject: Fixed (and changed) infoH.

The detection of new hypothesis was bugged.

Now infoH behaves like "Show Intros": it performs tac, grab
information on hypothesis names but let the state unchanged.

FTR: infoH is fundamentally unable to be correct in presence of
tactics that delete hypothesis and reuse there names. Like destruct or
induction. Fortunately destruct and induction now come with a variant
asking that the hypothesis is not deleted. To guess for the right
as-close for [induction H], do [infoH induction !H]. This will not
create the same names as induction would have by itself but at least
there will be the right number of hypothesis.
---
 proofs/refiner.ml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 974fa212f1..ba62b2cb2d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -186,10 +186,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
-(* Execute tac and show the names of hypothesis create by tac in
-   the "as" format. The resulting goals are printed *after* the
-   as-expression, which forces pg to some gymnastic. TODO: Have
-   something similar (better?) in the xml protocol. *)
+(* Execute tac, show the names of new hypothesis names created by tac
+   in the "as" format and then forget everything. From the logical
+   point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
+   except that it takes the time and memory of tac and prints "as"
+   information). The resulting (unchanged) goals are printed *after*
+   the as-expression, which forces pg to some gymnastic.
+   TODO: Have something similar (better?) in the xml protocol.
+   NOTE: some tactics delete hypothesis and reuse names (induction,
+   destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
   let oldhyps:Context.named_context = pf_hyps goal in
@@ -197,9 +202,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.named_context list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
+  let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
   let newhyps =
     List.map
-      (fun hypl -> List.subtract Context.eq_named_declaration hypl oldhyps)
+      (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
   let emacs_str s =
@@ -215,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   pp (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
       ++  (str (emacs_str "</infoH>")) ++ fnl());
-  rslt;;
+  tclIDTAC goal;;
 
 
 let catch_failerror (e, info) =
-- 
cgit v1.2.3


From 05be0a2eee49174c92f355edbdc0ffa6b44f0fac Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 21 Oct 2015 12:42:29 +0200
Subject: Bug #3956 is fixed.

---
 test-suite/bugs/closed/3956.v | 143 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 143 insertions(+)
 create mode 100644 test-suite/bugs/closed/3956.v

diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v
new file mode 100644
index 0000000000..c19a2d4a06
--- /dev/null
+++ b/test-suite/bugs/closed/3956.v
@@ -0,0 +1,143 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *)
+Set Universe Polymorphism.
+Set Primitive Projections.
+Close Scope nat_scope.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {A B} _ _.
+Arguments fst {A B} _ / .
+Arguments snd {A B} _ / .
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Unset Strict Universe Declaration.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z
+  := match p, q with idpath, idpath => idpath end.
+
+Definition path_prod {A B : Type} (z z' : A * B)
+: (fst z = fst z') -> (snd z = snd z') -> (z = z').
+Proof.
+  destruct z, z'; simpl; intros [] []; reflexivity.
+Defined.  
+
+Module Type TypeM.
+  Parameter m : Type2.
+End TypeM.
+
+Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM.
+  Definition m := XM.m * YM.m.
+End ProdM.
+
+Module Type FunctionM (XM YM : TypeM).
+  Parameter m : XM.m -> YM.m.
+End FunctionM.
+
+Module IdmapM (XM : TypeM) <: FunctionM XM XM.
+  Definition m := (fun x => x) : XM.m -> XM.m.
+End IdmapM.
+
+Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM).
+  Parameter m : forall x, fM.m x = gM.m x.
+End HomotopyM.
+
+Module ComposeM (XM YM ZM : TypeM)
+       (gM : FunctionM YM ZM) (fM : FunctionM XM YM)
+       <: FunctionM XM ZM.
+  Definition m := (fun x => gM.m (fM.m x)).
+End ComposeM.
+
+Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (gM : FunctionM XM ZM).
+  Parameter m : XM.m -> YM.m.
+  Parameter m_beta : forall x, fM.m (m x) = gM.m x.
+End CorecM.
+
+Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (hM kM : FunctionM XM YM).
+  Module fhM := ComposeM XM YM ZM fM hM.
+  Module fkM := ComposeM XM YM ZM fM kM.
+  Declare Module mM (pM : HomotopyM XM ZM fhM fkM)
+    : HomotopyM XM YM hM kM.
+End CoindpathsM.
+
+Module Type Comodality (XM : TypeM).
+  Parameter m : Type2.
+  Module mM <: TypeM.
+    Definition m := m.
+  End mM.
+  Parameter from : m -> XM.m.
+  Module fromM <: FunctionM mM XM.
+    Definition m := from.
+  End fromM.
+  Declare Module corecM : CorecM mM XM fromM.
+  Declare Module coindpathsM : CoindpathsM mM XM fromM.
+End Comodality.
+
+Module Comodality_Theory (F : Comodality).
+
+  Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module f_o_from_M <: FunctionM FXM.mM YM.
+      Definition m := fun x => fM.m (FXM.from x).
+    End f_o_from_M.
+    Module mM := FYM.corecM FXM.mM f_o_from_M.
+    Definition m := mM.m.
+  End F_functor_M.
+
+  Module F_prod_cmp_M (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module PM := ProdM XM YM.
+    Module PFM := ProdM FXM FYM.
+    Module fstM <: FunctionM PM XM.
+      Definition m := @fst XM.m YM.m.
+    End fstM.
+    Module sndM <: FunctionM PM YM.
+      Definition m := @snd XM.m YM.m.
+    End sndM.
+    Module FPM := F PM.
+    Module FfstM := F_functor_M PM XM fstM FPM FXM.
+    Module FsndM := F_functor_M PM YM sndM FPM FYM.
+    Definition m : FPM.m -> PFM.m
+      := fun z => (FfstM.m z , FsndM.m z).
+  End F_prod_cmp_M.
+
+  Module isequiv_F_prod_cmp_M
+         (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    (** The comparison map *)
+    Module cmpM := F_prod_cmp_M XM YM FXM FYM.
+    Module FPM := cmpM.FPM.
+    (** We construct an inverse to it using corecursion. *)
+    Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM.
+      Definition m : cmpM.PFM.m -> cmpM.PM.m
+        := fun z => ( FXM.from (fst z) , FYM.from (snd z) ).
+    End prod_from_M.
+    Module cmpinvM <: FunctionM cmpM.PFM FPM
+      := FPM.corecM cmpM.PFM prod_from_M.
+    (** We prove the first homotopy *)
+    Module cmpinv_o_cmp_M <: FunctionM FPM FPM
+      := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM.
+    Module idmap_FPM <: FunctionM FPM FPM
+      := IdmapM FPM.
+    Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
+    Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
+      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+      Proof.
+        intros x.
+        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+        apply path_prod@{i i i}; simpl.
+        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
+        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+      Defined.
+    End cip_FPHM.
+  End isequiv_F_prod_cmp_M.
+
+End Comodality_Theory.
\ No newline at end of file
-- 
cgit v1.2.3


From 95b04506542064fbda7a61c4b6ce276a668d25bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 21 Oct 2015 16:40:51 +0200
Subject: Mention bug 3199 fix as a source of incompatibilities.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 9f46131363..cf0f4446f4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -33,6 +33,9 @@ Tactics
   already do.
 - Importing Program no longer overrides the "exists" tactic (potential source
   of incompatibilities).
+- Hints costs are now correctly taken into account (potential source of
+  incompatibilities).
+
 
 API
 
-- 
cgit v1.2.3


From 273005ac85e9ae0c23328e243edeadfc8dcaf8bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2015 22:25:35 +0200
Subject: Fixing a bug in reporting ill-formed inductive.

Was introduced in b06d3badb (15 Jul 2015).
---
 kernel/indtypes.ml              | 2 +-
 test-suite/output/Inductive.out | 3 +++
 test-suite/output/Inductive.v   | 3 +++
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/Inductive.out
 create mode 100644 test-suite/output/Inductive.v

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d7a0bbf00..8b03df64c6 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -390,7 +390,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/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
new file mode 100644
index 0000000000..e912003f03
--- /dev/null
+++ b/test-suite/output/Inductive.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Last occurrence of "list'" must have "A" as 1st argument in
+ "A -> list' A -> list' (A * A)%type".
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
new file mode 100644
index 0000000000..8db8956e32
--- /dev/null
+++ b/test-suite/output/Inductive.v
@@ -0,0 +1,3 @@
+Fail Inductive list' (A:Set) : Set :=
+| nil' : list' A
+| cons' : A -> list' A -> list' (A*A).
-- 
cgit v1.2.3


From d30a7244b52e86c364320a8fa0794c7686f30074 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 23 Oct 2015 07:45:15 +0200
Subject: Support "Functional Scheme" in coqdoc. (Fix bug #4382)

---
 tools/coqdoc/cpretty.mll | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index cb70414675..d28921674b 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -320,6 +320,7 @@ let def_token =
   | "Instance"
   | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
+  | "Functional" space+ "Scheme"
 
 let decl_token =
   "Hypothesis"
-- 
cgit v1.2.3


From 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2015 09:57:50 +0200
Subject: Backtracking on interpreting toplevel calls to exact in scope
 determined by the type to prove (was introduced in 35846ec22, r15978, Nov
 2012).

Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.

Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...

See #4034 for a discussion.
---
 tactics/tacinterp.ml          |  4 +++-
 test-suite/bugs/closed/4034.v | 25 +++++++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4034.v

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5a0d26a1cb..6c125ed2d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -557,7 +557,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
       } in
-      intern_gen kind ~allow_patvar ~ltacvars env c
+      let kind_for_intern =
+        match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
+      intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
diff --git a/test-suite/bugs/closed/4034.v b/test-suite/bugs/closed/4034.v
new file mode 100644
index 0000000000..3f7be4d1c7
--- /dev/null
+++ b/test-suite/bugs/closed/4034.v
@@ -0,0 +1,25 @@
+(* This checks compatibility of interpretation scope used for exact
+   between 8.4 and 8.5. See discussion at
+   https://coq.inria.fr/bugs/show_bug.cgi?id=4034. It is not clear
+   what we would like exactly, but certainly, if exact is interpreted
+   in a special scope, it should be interpreted consistently so also
+   in ltac code. *)
+
+Record Foo := {}.
+Bind Scope foo_scope with Foo.
+Notation "!" := Build_Foo : foo_scope.
+Notation "!" := 1 : core_scope.
+Open Scope foo_scope.
+Open Scope core_scope.
+
+Goal Foo.
+  Fail exact !.
+(* ... but maybe will we want it to succeed eventually if we ever
+   would be able to make it working the same in
+
+Ltac myexact e := exact e.
+
+Goal Foo.
+  myexact !.
+Defined.
+*)
-- 
cgit v1.2.3


From 1b029b2163386f20179a61f6bdb68e5532f4c306 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2015 12:01:26 +0200
Subject: Fixing a loop in checking hints with holes.

For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
---
 tactics/hints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2755ed9cb0..4ba9adafec 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1071,7 +1071,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
-      if not (Int.Set.is_empty (free_rels t)) then
+      if not (closed0 c) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential t then
 	(* Not clever enough to construct dependency graph of evars *)
-- 
cgit v1.2.3


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/mod_typing.ml  | 2 +-
 kernel/mod_typing.mli | 3 +++
 kernel/modops.ml      | 4 ----
 kernel/modops.mli     | 3 ---
 kernel/safe_typing.ml | 8 ++------
 toplevel/himsg.ml     | 4 ----
 6 files changed, 6 insertions(+), 18 deletions(-)

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 922652287b..eef83ce743 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -359,4 +359,4 @@ let rec translate_mse_incl env mp inl = function
   |MEapply (fe,arg) ->
     let ftrans = translate_mse_incl 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 *)
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 80db12b0d3..0c3fb2ba79 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -36,6 +36,9 @@ val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
+(** [translate_mse_incl] translate the mse of a real module (no
+    module type here) given to an Include *)
+
 val translate_mse_incl :
   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..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) =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8efc36df72..8f380830db 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -924,9 +924,6 @@ let explain_label_missing l s =
   str "The field " ++ str (Label.to_string l) ++ str " is missing in "
   ++ str s ++ str "."
 
-let explain_higher_order_include () =
-  str "You cannot Include a higher-order structure."
-
 let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
   | LabelAlreadyDeclared l -> explain_label_already_declared l
@@ -943,7 +940,6 @@ 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
-  | HigherOrderInclude -> explain_higher_order_include ()
 
 (* Module internalization errors *)
 
-- 
cgit v1.2.3


From 83e82ef7b42f47d63d3b40b2698695a0e7b2d685 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 25 Oct 2015 14:58:39 +0100
Subject: Safe_typing: add clean_bounded_mod_expr in Include Self of modtype
 (fix #4331)

---
 kernel/mod_typing.ml  | 12 ++++++++++--
 kernel/mod_typing.mli | 14 +++++++-------
 kernel/safe_typing.ml |  9 ++-------
 3 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index eef83ce743..c03c5175fd 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)
   |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 0c3fb2ba79..bc0e20205a 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -36,14 +36,14 @@ val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
-(** [translate_mse_incl] translate the mse of a real module (no
-    module type here) given to an Include *)
-
-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/safe_typing.ml b/kernel/safe_typing.ml
index fdacbb365c..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  *)
-- 
cgit v1.2.3


From 6417a9e72feb39b87f0b456186100b11d1c87d5f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 25 Oct 2015 16:40:32 +0100
Subject: Declaremods: replace two anomalies by user errors (fix #3974 and
 #3975)

 As shown by the code snippets in these bug reports, I've been too
 hasty in considering these situations as anomalies in commit 466c4cb
 (at least the one at the last line of consistency_checks). So let's turn
 these anomalies back to regular user errors, as they were before this commit.
---
 library/declaremods.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index f66656d09a..7f607a51c9 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -166,12 +166,14 @@ let consistency_checks exists dir dirinfo =
     let globref =
       try Nametab.locate_dir (qualid_of_dirpath dir)
       with Not_found ->
-        anomaly (pr_dirpath dir ++ str " should already exist!")
+        errorlabstrm "consistency_checks"
+          (pr_dirpath dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      anomaly (pr_dirpath dir ++ str " already exists")
+      errorlabstrm "consistency_checks"
+        (pr_dirpath dir ++ str " already exists")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
-- 
cgit v1.2.3