From eb479438328a473ff1cf5fe010ed714194dbf28f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 00:50:19 +0200
Subject: [pp] Fix newline issues.

This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where
we got a few cases wrong wrt to newline endings.

Thanks to @herbelin for pointing it out.

This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
---
 pretyping/reductionops.ml | 4 ++--
 proofs/refiner.ml         | 2 +-
 toplevel/vernac.ml        | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b61..8259876c29 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
              (h 0 (str "<<" ++ Termops.print_constr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
 		   str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
-		   str ">>") ++ fnl ())
+		   str ">>"))
     in
     let fold () =
       let () = if !debug_RAKAM then
-	  let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
+	  let open Pp in Feedback.msg_notice (str "<><><><><>") in
       (s,cst_l)
     in
     match kind_of_term x with
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ebd30820be..ea8543b02f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -221,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   Feedback.msg_notice
     (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")) ++ fnl());
+      ++  (str (emacs_str "</infoH>")));
   tclIDTAC goal;;
 
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f83ada466b..0fc56353e8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,7 +101,7 @@ let verbose_phrase verbch loc =
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        Feedback.msg_notice (str s ++ fnl ())
+        Feedback.msg_notice (str s)
     | None -> ()
 
 exception End_of_input
-- 
cgit v1.2.3


From 01ce1ddffeba4127bcd37938525a8fe31e6f1cee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:07:57 +0200
Subject: [pp] Fix bug 4842 (Time prints in multiple lines)

This commit proposes a fix for
https://coq.inria.fr/bugs/show_bug.cgi?id=4842

The previous feature is a bit complicated to do correctly due to the
separation over who has control of the console.

Indeed, `-timed` is a command line option of the batch compiler, so we
resort to a hack and assume control over the console. I am not very
happy with this solution but should do the job.

Note that the timing event is still being sent by the standard msg
mechanism. A particular point of interest is the duplication of paths
between the stm and vernac.
---
 toplevel/vernac.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f83ada466b..b4926cf786 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -158,7 +158,7 @@ let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let display_cmd_header loc com =
+let pp_cmd_header loc com =
   let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
   let noblank s =
     for i = 0 to String.length s - 1 do
@@ -173,11 +173,15 @@ let display_cmd_header loc com =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
-  in
-  Feedback.msg_notice
-    (str "Chars " ++ int start ++ str " - " ++ int stop ++
-     str " [" ++ str cmd ++ str "] ")
+  in str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] "
 
+(* This is a special case where we assume we are in console batch mode
+   and take control of the console.
+ *)
+let print_cmd_header loc com =
+  Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
+  Format.pp_print_flush !Pp_control.std_ft ()
 
 let rec vernac_com checknav (loc,com) =
   let interp = function
@@ -208,7 +212,8 @@ let rec vernac_com checknav (loc,com) =
     try
       checknav loc com;
       if do_beautify () then pr_new_syntax loc (Some com);
-      if !Flags.time then display_cmd_header loc com;
+      (* XXX: This is not 100% correct if called from an IDE context *)
+      if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
       let a = CLexer.com_state () in
       interp com;
-- 
cgit v1.2.3


From 00808a1fa05e34fee36b8dfff4e7c72943b22c23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 18:54:39 +0200
Subject: Short path for Pretyping.ltac_interp_name_env.

Instead of recomputing the evar name environment from scratch when it is
unchanged, we simply return the original one.

This should fix #4964 for good, although I still find the global evar naming
mechanism from Pretyping more than messy. Introducing the heuristic allowing
to capture variables from Ltac in constr binders is indeed the root of many
evils... That is far from being a zero-cost abstraction!
---
 pretyping/pretyping.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ef96e0344..e7f87c5f71 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -403,9 +403,10 @@ let ltac_interp_name_env k0 lvar env =
   (* tail is the part of the env enriched by pretyping *)
   let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
-  let env = pop_rel_context n env in
-  let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
-  push_rel_context ctxt env
+  let open Context.Rel.Declaration in
+  let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+  if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
+  else push_rel_context ctxt' (pop_rel_context n env)
 
 let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
-- 
cgit v1.2.3


From b1791fe718eae95897d2dbd160b05285c6df239c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 19:33:03 +0200
Subject: Do not recompute the whole evar naming environment in GProd
 intepretation.

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e7f87c5f71..f466740036 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -804,8 +804,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let j = pretype_type empty_valcon env evdref lvar c2 in
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
-        let var = (name,j.utj_val) in
-        let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
+        let var = LocalAssum (name, j.utj_val) in
+        let env' = push_rel var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
     let name = ltac_interp_name lvar name in
-- 
cgit v1.2.3


From 1948023891d26e628397a303263b912225f2cc31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 21 Aug 2016 22:09:01 +0200
Subject: Documenting "Set Structural Injection".

---
 doc/refman/RefMan-tac.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 21b72b8eff..b668239a6a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2280,6 +2280,15 @@ hypothesis.
 
 \end{Variants}
 
+\optindex{Structural Injection}
+
+It is possible to ensure that \texttt{injection {\term}} erases the
+original hypothesis and leaves the generated equalities in the context
+rather than putting them as antecedents of the current goal, as if
+giving \texttt{injection {\term} as} (with an empty list of names). To
+obtain this behavior, the option {\tt Set Structural Injection} must
+be activated. This option is off by default.
+
 \subsection{\tt inversion \ident}
 \tacindex{inversion}
 
-- 
cgit v1.2.3


From 687d510cb43db5029fb4545c3b12ac20cf99197a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 22 Aug 2016 11:11:41 +0200
Subject: Pushing error backtrace in unification reraise.

---
 pretyping/unification.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f8..6d80db6455 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1080,8 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
     a
   with e ->
+    let e = CErrors.push e in
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
-    raise e
+    iraise e
 
 
 let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
-- 
cgit v1.2.3


From 5ede69c8e67e6de34af2850695ae7ee24f8588ea Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 20 Aug 2016 01:11:55 +0200
Subject: Use a better data structure for VM compilation of free vars.

This fixes #3450 and probably provides a huge speed-up to many instances.
---
 kernel/cbytecodes.ml  | 20 +++++++++++++++++++-
 kernel/cbytecodes.mli |  5 ++++-
 kernel/cbytegen.ml    | 33 ++++++++++++++-------------------
 3 files changed, 37 insertions(+), 21 deletions(-)

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004f..8d4de523a1 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -142,11 +142,29 @@ type fv = fv_elem array
 exception NotClosed
 
 
+module Fv_elem =
+struct
+type t = fv_elem
+
+let compare e1 e2 = match e1, e2 with
+| FVnamed id1, FVnamed id2 -> Id.compare id1 id2
+| FVnamed _, _ -> -1
+| FVrel _, FVnamed _ -> 1
+| FVrel r1, FVrel r2 -> Int.compare r1 r2
+| FVrel _, FVuniv_var _ -> -1
+| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
+| FVuniv_var i1, _ -> 1
+
+end
+
+module FvMap = Map.Make(Fv_elem)
+
 (*spiwack: both type have been moved from Cbytegen because I needed then
   for the retroknowledge *)
 type vm_env = {
     size : int;              (* longueur de la liste [n] *)
-    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+    fv_rev : fv_elem list;   (* [fvn; ... ;fv1] *)
+    fv_fwd : int FvMap.t;    (* reverse mapping *)
   }
 
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 6fa0841af9..5f1f09d00c 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -139,11 +139,14 @@ type fv = fv_elem array
             closed terms. *)
 exception NotClosed
 
+module FvMap : Map.S with type key = fv_elem
+
 (*spiwack: both type have been moved from Cbytegen because I needed them
   for the retroknowledge *)
 type vm_env = {
     size : int;              (** length of the list [n] *)
-    fv_rev : fv_elem list    (** [fvn; ... ;fv1] *)
+    fv_rev : fv_elem list;   (** [fvn; ... ;fv1] *)
+    fv_fwd : int FvMap.t;    (** reverse mapping *)
   }
 
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2d1ae68f4b..008955d804 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -93,7 +93,12 @@ open Pre_env
 
 type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
 
-let empty_fv = { size= 0;  fv_rev = [] }
+let empty_fv = { size= 0;  fv_rev = []; fv_fwd = FvMap.empty }
+let push_fv d e = {
+  size = e.size + 1;
+  fv_rev = d :: e.fv_rev;
+  fv_fwd = FvMap.add d e.size e.fv_fwd;
+}
 
 let fv r = !(r.in_env)
 
@@ -184,20 +189,15 @@ let push_local sz r =
     in_stack = (sz + 1) :: r.in_stack }
 
 (*i Compilation of variables *)
-let find_at f l =
-  let rec aux n = function
-    | [] -> raise Not_found
-    | hd :: tl -> if f hd then n else aux (n + 1) tl
-  in aux 1 l
+let find_at fv env = FvMap.find fv env.fv_fwd
 
 let pos_named id r =
   let env = !(r.in_env) in
   let cid = FVnamed id in
-  let f = function FVnamed id' -> Id.equal id id' | _ -> false in
-  try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+  try Kenvacc(r.offset + find_at cid env)
   with Not_found ->
     let pos = env.size in
-    r.in_env := { size = pos+1; fv_rev =  cid:: env.fv_rev};
+    r.in_env := push_fv cid env;
     Kenvacc (r.offset + pos)
 
 let pos_rel i r sz =
@@ -212,11 +212,10 @@ let pos_rel i r sz =
       let i = i - r.nb_rec in
       let db = FVrel(i) in
       let env = !(r.in_env) in
-      let f = function FVrel j -> Int.equal i j | _ -> false in
-      try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+      try Kenvacc(r.offset + find_at db env)
       with Not_found ->
 	let pos = env.size in
-	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
+	r.in_env := push_fv db env;
 	Kenvacc(r.offset + pos)
 
 let pos_universe_var i r sz =
@@ -224,15 +223,11 @@ let pos_universe_var i r sz =
     Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
   else
     let env = !(r.in_env) in
-    let f = function
-      | FVuniv_var u -> Int.equal i u
-      | _ -> false
-    in
-    try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+    let db = FVuniv_var i in
+    try Kenvacc (r.offset + find_at db env)
     with Not_found ->
       let pos = env.size in
-      let db = FVuniv_var i in
-      r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+      r.in_env := push_fv db env;
       Kenvacc(r.offset + pos)
 
 (*i  Examination of the continuation *)
-- 
cgit v1.2.3


From fb9dfa53f2f71ed501be27213600143ee0b7554d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 22 Aug 2016 17:13:14 +0200
Subject: Fast path for set operations.

We consider an approximation of the size of sets before choosing the most
appropriate algorithm. This drastically affects some universe-polymorphic
code which was doing a lot of set operations on disimilar sizes.
---
 lib/cMap.ml  |   6 ++++
 lib/cMap.mli |   3 ++
 lib/hMap.ml  | 101 ++++++++++++++++++++++++++++++++++++++++++++++-------------
 3 files changed, 89 insertions(+), 21 deletions(-)

diff --git a/lib/cMap.ml b/lib/cMap.ml
index 4b058380c6..ba0873ffa7 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -34,6 +34,7 @@ sig
   val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  val height : 'a t -> int
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -57,6 +58,7 @@ sig
   val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a map -> 'a map
   val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  val height : 'a map -> int
   module Unsafe :
   sig
     val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
@@ -168,6 +170,10 @@ struct
     if l == l' && r == r' && v == v' then s
     else map_inj (MNode (l', k, v', r', h))
 
+  let height s = match map_prj s with
+  | MEmpty -> 0
+  | MNode (_, _, _, _, h) -> h
+
   module Unsafe =
   struct
 
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 3ef7fa2c8a..2838b374ec 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -61,6 +61,9 @@ sig
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
   (** As [mapi] but tries to preserve sharing. *)
 
+  val height : 'a t -> int
+  (** An indication of the logarithmic size of a map *)
+
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
diff --git a/lib/hMap.ml b/lib/hMap.ml
index 778c366fd5..ea76e74272 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -68,34 +68,91 @@ struct
         Int.Map.update h m s
     with Not_found -> s
 
+  let height s = Int.Map.height s
+
+  let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+  (** Assumes s1 << s2 *)
+  let fast_union s1 s2 =
+    let fold h s accu =
+      try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+      with Not_found -> Int.Map.add h s accu
+    in
+    Int.Map.fold fold s1 s2
+
   let union s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | (Some _ as m), None | None, (Some _ as m) -> m
-    | Some m1, Some m2 -> Some (Set.union m1 m2)
+    if is_smaller s1 s2 then fast_union s1 s2
+    else if is_smaller s2 s1 then fast_union s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None | None, (Some _ as m) -> m
+      | Some m1, Some m2 -> Some (Set.union m1 m2)
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_inter s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> Set.mem e s') s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> accu
     in
-    Int.Map.merge fu s1 s2
+    Int.Map.fold fold s1 Int.Map.empty
 
   let inter s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | Some _, None | None, Some _ -> None
-    | Some m1, Some m2 ->
-      let m = Set.inter m1 m2 in
-      if Set.is_empty m then None else Some m
+    if is_smaller s1 s2 then fast_inter s1 s2
+    else if is_smaller s2 s1 then fast_inter s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | Some _, None | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.inter m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_diff_l s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> not (Set.mem e s')) s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> Int.Map.add h s accu
+    in
+    Int.Map.fold fold s1 Int.Map.empty
+
+  (** Assumes s2 << s1 *)
+  let fast_diff_r s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h accu in
+        let si = Set.filter (fun e -> not (Set.mem e s)) s' in
+        if Set.is_empty si then Int.Map.remove h accu
+        else Int.Map.update h si accu
+     with Not_found -> accu
     in
-    Int.Map.merge fu s1 s2
+    Int.Map.fold fold s2 s1
 
   let diff s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | (Some _ as m), None -> m
-    | None, Some _ -> None
-    | Some m1, Some m2 ->
-      let m = Set.diff m1 m2 in
-      if Set.is_empty m then None else Some m
-    in
-    Int.Map.merge fu s1 s2
+    if is_smaller s1 s2 then fast_diff_l s1 s2
+    else if is_smaller s2 s2 then fast_diff_r s1 s2
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None -> m
+      | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.diff m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
 
   let compare s1 s2 = Int.Map.compare Set.compare s1 s2
 
@@ -324,6 +381,8 @@ struct
     let fs m = Map.smartmapi f m in
     Int.Map.smartmap fs s
 
+  let height s = Int.Map.height s
+
   module Unsafe =
   struct
     let map f s =
-- 
cgit v1.2.3


From f0ba692422a8a608ef44964ecf74d8b483c1beb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Aug 2016 11:28:29 +0200
Subject: Fix bug #4904: [Import] does not load intermediately unqualified
 names of aliases.

---
 interp/syntax_def.ml          |  2 +-
 test-suite/bugs/closed/4904.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4904.v

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f96d8acc10..d2dcbd92aa 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function
       false
 
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  if not (is_alias_of_already_visible_name sp pat) then begin
+  if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
     Nametab.push_syndef (Nametab.Exactly i) sp kn;
     match onlyparse with
     | None ->
diff --git a/test-suite/bugs/closed/4904.v b/test-suite/bugs/closed/4904.v
new file mode 100644
index 0000000000..a47c3b07a9
--- /dev/null
+++ b/test-suite/bugs/closed/4904.v
@@ -0,0 +1,11 @@
+Module A.
+Module B.
+Notation mynat := nat.
+Notation nat := nat.
+End B.
+End A.
+
+Print A.B.nat. (* Notation A.B.nat := nat *)
+Import A.
+Print B.mynat.
+Print B.nat.
-- 
cgit v1.2.3


From 50bece7c25e62132bc06c3bb0261937c657319d3 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 22 Aug 2016 15:31:24 -0400
Subject: update Proof General URL

---
 doc/faq/fk.bib            | 2 +-
 doc/refman/RefMan-uti.tex | 2 +-
 doc/refman/biblio.bib     | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 4d90efcdb1..3410427dee 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -2171,7 +2171,7 @@ Decomposition}},
 @Misc{ProofGeneral,
   author =	 {David Aspinall},
   title =	 {Proof General},
-  note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
+  note =	 {\url{https://proofgeneral.github.io/}}
 }
 
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5c..10271ce0ca 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
 files.
 
 {\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
 
 
 \section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f0..e69725838e 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
 @Misc{ProofGeneral,
   author      = {David Aspinall},
   title       = {Proof General},
-  note        = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+  note        = {\url{https://proofgeneral.github.io/}}
 }
 
 @Book{CoqArt,
-- 
cgit v1.2.3


From fa7d01708e4af53a6adeddf563b57bc38fc8d2fe Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 23 Aug 2016 15:09:56 +0200
Subject: fix get_host_port error message (#4724)

---
 toplevel/coqtop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c49a97cadb..a56459f180 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -382,7 +382,7 @@ let get_host_port opt s =
        Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
   | ["stdfds"] -> Some Spawned.AnonPipe
   | _ ->
-     prerr_endline ("Error: host:port or stdfds expected after option "^opt);
+     prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
      exit 1
 
 let get_error_resilience opt = function
-- 
cgit v1.2.3


From 940a6286b62a095f3d6a0f3d4851f56583a852c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 23 Aug 2016 16:55:56 +0200
Subject: Arguments: give / after last ! error detection fixed

---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f69c4fa186..f87fa8a447 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1064,7 +1064,7 @@ let vernac_declare_arguments locality r l nargs flags =
     vernac_declare_implicits locality r []
   else if some_implicits_specified || List.mem `ClearImplicits flags then
     vernac_declare_implicits locality r implicits;
-  if nargs >= 0 && nargs < List.fold_left max 0 rargs then
+  if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then
     error "The \"/\" option must be placed after the last \"!\".";
   let no_flags = List.is_empty flags in
   let rec narrow = function
-- 
cgit v1.2.3


From 7799de316e12878ef47fb74fcb4ec9533005a6dc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Aug 2016 23:58:15 +0200
Subject: Fix bug #4914: LtacProf printout has too many newlines.

---
 ltac/profile_ltac.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index bea02e3dcb..fb71becfc3 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -235,7 +235,6 @@ let rec print_node all_total indent prefix (s, n) =
     ++ padl 8 (string_of_int e.ncalls)
     ++ padl 10 (format_sec (e.max_total))
   ) ++
-  fnl () ++
   print_table all_total indent false n.children
 
 and print_table all_total indent first_level table =
-- 
cgit v1.2.3


From 433d042350f7d7e52f9ef5def0f9405218cb109b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 24 Aug 2016 06:59:19 +0200
Subject: Properly compute types for assumed section variables (bug #5035).

This bug was introduced by

commit 34ef02fac1110673ae74c41c185c228ff7876de2
Author: Matej Kosik <m4tej.kosik@gmail.com>
Date:   Fri Jan 29 10:13:12 2016 +0100

    CLEANUP: Context.{Rel,Named}.Declaration.t
---
 toplevel/assumptions.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 30b7f299f8..45c539e229 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -283,7 +283,9 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
   let fold obj _ accu = match obj with
   | VarRef id ->
     let decl = Global.lookup_named id in
-    if is_local_assum decl then ContextObjectMap.add (Variable id) t accu
+    if is_local_assum decl then
+      let t = Context.Named.Declaration.get_type decl in
+      ContextObjectMap.add (Variable id) t accu
     else accu
   | ConstRef kn ->
       let cb = lookup_constant kn in
-- 
cgit v1.2.3


From dd4654ce6f1808cc19c701219b4bad120b7f2271 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Aug 2016 01:57:31 +0200
Subject: Do not export an internal function in Namegen.

---
 engine/namegen.mli        | 3 ---
 toplevel/vernacentries.ml | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/engine/namegen.mli b/engine/namegen.mli
index e5c156b4e5..97c7c34a56 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -64,9 +64,6 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
    but tolerate overwriting section variables, as in goals *)
 val next_global_ident_away : Id.t -> Id.t list -> Id.t
 
-(** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t
-
 (** Default is [default_non_dependent_ident] *)
 val next_name_away  : Name.t -> Id.t list -> Id.t
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f87fa8a447..dc098f1f00 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -135,7 +135,7 @@ let make_cases s =
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
-		   let n' = Namegen.next_name_away_in_cases_pattern ([],mkMeta 0) n avoid in
+		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
 		   Id.to_string n' :: rename (n'::avoid) l in
 	     let al' = rename [] al in
 	     (Id.to_string consname :: al') :: l)
-- 
cgit v1.2.3


From 7244637f251272c0d0155d49fc7c1af255b7cef8 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 25 Aug 2016 13:53:00 +0200
Subject: FIX: Coq version

---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index d152c406ee..2c1d531ead 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,7 +11,7 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "trunk"
+let coq_version = "8.6.0"
 let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8511
-- 
cgit v1.2.3