From 5b4e3ace20eb2ab569d172a1f358f26f451d361c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 29 Dec 2015 13:27:36 -0500
Subject: Move compatibility notations to their proper files

---
 theories/Compat/Coq84.v | 16 ----------------
 theories/ZArith/Int.v   |  4 ++++
 2 files changed, 4 insertions(+), 16 deletions(-)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 1c70a894a5..62b8a03989 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -53,21 +53,5 @@ Tactic Notation "esplit" := esplit.
 
 Global Set Regular Subst Tactic.
 
-(** Some names have changed in the standard library, so we add aliases. *)
-Require Coq.ZArith.Int.
-Module Export Coq.
-  Module Export ZArith.
-    Module Int.
-      Module Z_as_Int.
-        Include Coq.ZArith.Int.Z_as_Int.
-        (* FIXME: Should these get a (compat "8.4")?  Or be moved to Z_as_Int, probably? *)
-        Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing).
-        Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing).
-        Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing).
-      End Z_as_Int.
-    End Int.
-  End ZArith.
-End Coq.
-
 (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
 Require Coq.Numbers.Natural.Peano.NPeano.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index d210792f9a..b78891c711 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -451,4 +451,8 @@ Module Z_as_Int <: Int.
   Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p).
   Proof. reflexivity. Qed.
 
+  (** Compatibility notations for Coq v8.4 *)
+  Notation plus := Coq.ZArith.Int.Z_as_Int.add (compat "8.4").
+  Notation minus := Coq.ZArith.Int.Z_as_Int.sub (compat "8.4").
+  Notation mult := Coq.ZArith.Int.Z_as_Int.mul (compat "8.4").
 End Z_as_Int.
-- 
cgit v1.2.3


From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: Avoid infinite loop/stack overflow when using "simpl nomatch" (bug
 #4576).

When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.

Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
---
 pretyping/reductionops.ml     | 6 ++++--
 test-suite/bugs/closed/4576.v | 3 +++
 2 files changed, 7 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4576.v

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 13b7fb4079..7c7b31395e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -811,7 +811,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     let fold () =
       let () = if !debug_RAKAM then
 	  let open Pp in pp (str "<><><><><>" ++ fnl ()) in
-      if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+      (s,cst_l)
     in
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
@@ -1002,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
-  whrec (Option.default Cst_stack.empty csts)
+  fun xs ->
+  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
+  if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 0000000000..2c643ea779
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
-- 
cgit v1.2.3


From 857e9ff0a7927d370c8a16e723385a9b199de872 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 16:54:38 +0200
Subject: Properly handle notations containing spaces (bug #4538).

When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
---
 test-suite/bugs/closed/4538.v |  1 +
 toplevel/metasyntax.ml        | 23 +++++++++++++++++------
 2 files changed, 18 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/4538.v

diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v
new file mode 100644
index 0000000000..f925aae9e5
--- /dev/null
+++ b/test-suite/bugs/closed/4538.v
@@ -0,0 +1 @@
+Reserved Notation "   (u *)   ".
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 231b22e255..2ccd27acb9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1002,7 +1002,7 @@ let make_interpretation_vars recvars allvars =
     (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars
 
 let check_rule_productivity l =
-  if List.for_all (function NonTerminal _ -> true | _ -> false) l then
+  if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
     error "A notation must include at least one symbol.";
   if (match l with SProdList _ :: _ -> true | _ -> false) then
     error "A recursive notation must start with at least one symbol."
@@ -1020,8 +1020,21 @@ let is_not_printable onlyparse noninjective = function
   else onlyparse
 
 let find_precedence lev etyps symbols =
-  match symbols with
-  | NonTerminal x :: _ ->
+  let first_symbol =
+    let rec aux = function
+      | Break _ :: t -> aux t
+      | h :: t -> h
+      | [] -> assert false (* rule is known to be productive *) in
+    aux symbols in
+  let last_is_terminal () =
+    let rec aux b = function
+      | Break _ :: t -> aux b t
+      | Terminal _ :: t -> aux true t
+      | _ :: t -> aux false t
+      | [] -> b in
+    aux false symbols in
+  match first_symbol with
+  | NonTerminal x ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
@@ -1044,9 +1057,7 @@ let find_precedence lev etyps symbols =
 	if Option.is_empty lev then
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
-  | Terminal _ ::l when
-      (match List.last symbols with Terminal _ -> true |_ -> false)
-      ->
+  | Terminal _ when last_is_terminal () ->
       if Option.is_empty lev then
 	([msg_info,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
-- 
cgit v1.2.3


From a165495c957e7a2a22a9b1704114222bf615b869 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 17:50:52 +0200
Subject: Make votour a bit more robust/forgiving with respect to user commands
 (bug #4702).

---
 checker/votour.ml | 48 +++++++++++++++++++++++++++++++++---------------
 1 file changed, 33 insertions(+), 15 deletions(-)

diff --git a/checker/votour.ml b/checker/votour.ml
index 78978bb267..ec8892d5bd 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,6 +10,26 @@ open Values
 
 (** {6 Interactive visit of a vo} *)
 
+let rec read_num max =
+  let quit () =
+    Printf.printf "\nGoodbye!\n%!";
+    exit 0 in
+  Printf.printf "# %!";
+  let l = try read_line () with End_of_file -> quit () in
+  if l = "u" then None
+  else if l = "x" then quit ()
+  else
+    try
+      let v = int_of_string l in
+      if v < 0 || v >= max then
+        let () =
+          Printf.printf "Out-of-range input! (only %d children)\n%!" max in
+        read_num max
+      else Some v
+    with Failure "int_of_string" ->
+      Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
+      read_num max
+
 type 'a repr =
 | INT of int
 | STRING of string
@@ -246,15 +266,13 @@ let rec visit v o pos =
     (fun i vop -> Printf.printf "  %d: %s\n" i (node_info vop))
     children;
   Printf.printf "-------------\n";
-  Printf.printf ("# %!");
-  let l = read_line () in
   try
-    if l = "u" then let info = pop () in visit info.typ info.obj info.pos
-    else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0)
-    else
-      let v',o',pos' = children.(int_of_string l) in
-      push (get_name v) v o pos;
-      visit v' o' pos'
+    match read_num (Array.length children) with
+    | None -> let info = pop () in visit info.typ info.obj info.pos
+    | Some child ->
+       let v',o',pos' = children.(child) in
+       push (get_name v) v o pos;
+       visit v' o' pos'
   with
   | Failure "empty stack" -> ()
   | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
@@ -341,13 +359,13 @@ let visit_vo f =
       let size = if Sys.word_size = 64 then header.size64 else header.size32 in
       Printf.printf "  %d: %s, starting at byte %d (size %iw)\n" i name pos size)
       segments;
-    Printf.printf "# %!";
-    let l = read_line () in
-    let seg = int_of_string l in
-    seek_in ch segments.(seg).pos;
-    let o = Repr.input ch in
-    let () = Visit.init () in
-    Visit.visit segments.(seg).typ o []
+    match read_num (Array.length segments) with
+    | Some seg ->
+       seek_in ch segments.(seg).pos;
+       let o = Repr.input ch in
+       let () = Visit.init () in
+       Visit.visit segments.(seg).typ o []
+    | None -> ()
   done
 
 let main =
-- 
cgit v1.2.3


From 24a125b779c0cf6e9b0662e122c74aa80eb1837b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 08:21:36 +0200
Subject: Remove extraneous space in coqtop/pg output (bug #4675).

---
 plugins/decl_mode/g_decl_mode.ml4 | 19 ++++++++-----------
 printing/printer.ml               | 16 ++++++----------
 test-suite/output/Intuition.out   |  2 +-
 test-suite/output/Naming.out      | 40 +++++++++++++++++++--------------------
 test-suite/output/Quote.out       | 18 +++++++++---------
 test-suite/output/set.out         |  6 +++---
 test-suite/output/simpl.out       |  6 +++---
 7 files changed, 50 insertions(+), 57 deletions(-)

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b62cfd6add..4c5c65669a 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -24,17 +24,14 @@ open Ppdecl_proof
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let preamb,thesis,penv,pc =
-    (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
-    (str "thesis := "  ++ fnl ()),
-    Printer.pr_context_of env sigma,
-    Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
-  in
-    preamb ++
-    str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (Printer.emacs_str "")  ++
-		       str "============================" ++ fnl ()  ++
-		       thesis ++ str " " ++  pc) ++ fnl ()
+  let concl = Goal.V82.concl sigma g in
+  let goal =
+    Printer.pr_context_of env sigma ++ cut () ++
+      str "============================" ++ cut ()  ++
+      str "thesis :=" ++ cut () ++
+      Printer.pr_goal_concl_style_env env sigma concl in
+  str "     *** Declarative Mode ***" ++ fnl () ++ fnl () ++
+    str "  " ++ v 0 goal
 
 let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
   match gll with
diff --git a/printing/printer.ml b/printing/printer.ml
index 4e740bffe2..8469490f05 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -381,16 +381,12 @@ let pr_transparent_state (ids, csts) =
 let default_pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let preamb,thesis,penv,pc =
-    mt (), mt (),
-    pr_context_of env sigma,
-    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
-  in
-    preamb ++
-    str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (emacs_str "")  ++
-		       str "============================" ++ fnl ()  ++
-		       thesis ++ str " " ++  pc)
+  let concl = Goal.V82.concl sigma g in
+  let goal =
+    pr_context_of env sigma ++ cut () ++
+      str "============================" ++ cut ()  ++
+      pr_goal_concl_style_env env sigma concl in
+  str "  " ++ v 0 goal
 
 (* display a goal tag *)
 let pr_goal_tag g =
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fdebc..f2bf25ca65 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -3,4 +3,4 @@
   m, n : Z
   H : (m >= n)%Z
   ============================
-   (m >= m)%Z
+  (m >= m)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index f0d2562e0f..c142d28ebe 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -2,40 +2,40 @@
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
-   x + x1 = x4 + x0
+  x + x1 = x4 + x0
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
-   x + x1 = x4 + x0 -> foo (S x)
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
+  x + x1 = x4 + x0 -> foo (S x)
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   ============================
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -44,7 +44,7 @@
       forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   ============================
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -54,10 +54,10 @@
   H0 : x + x1 = x4 + x0
   x5, x6, x7, S : nat
   ============================
-   x5 + S = x6 + x7 + Datatypes.S x
+  x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, a : nat
   H : a = 0 -> forall a : nat, a = 0
   ============================
-   a = 0
+  a = 0
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
index ca7fc3624b..998eb37cc8 100644
--- a/test-suite/output/Quote.out
+++ b/test-suite/output/Quote.out
@@ -8,17 +8,17 @@
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f
-     (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
-     (f_and (f_atom (Left_idx End_idx))
-        (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
-           (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+  interp_f
+    (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+    (f_and (f_atom (Left_idx End_idx))
+       (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+          (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
 1 subgoal
   
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-     (f_and (f_const A)
-        (f_and (f_or (f_atom End_idx) (f_const A))
-           (f_or (f_const A) (f_not (f_atom End_idx)))))
+  interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+    (f_and (f_const A)
+       (f_and (f_or (f_atom End_idx) (f_const A))
+          (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc220..4b72d73eb3 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -3,16 +3,16 @@
   y1 := 0 : nat
   x := 0 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2 := 0 : nat
   x := y2 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2, y3 := 0 : nat
   x := y2 + y3 : nat
   ============================
-   x = x
+  x = x
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 73888da9a0..526e468f5b 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -2,14 +2,14 @@
   
   x : nat
   ============================
-   x = S x
+  x = S x
 1 subgoal
   
   x : nat
   ============================
-   0 + x = S x
+  0 + x = S x
 1 subgoal
   
   x : nat
   ============================
-   x = 1 + x
+  x = 1 + x
-- 
cgit v1.2.3


From f51dca0647b3213eb20a9b004372e5e6182bb29a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 11:02:05 +0200
Subject: Call hooks when terminating a definition proof (bug #4663).

Also register properly the kind of definition.
---
 test-suite/bugs/closed/4663.v | 3 +++
 toplevel/vernacentries.ml     | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4663.v

diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v
new file mode 100644
index 0000000000..b76619882a
--- /dev/null
+++ b/test-suite/bugs/closed/4663.v
@@ -0,0 +1,3 @@
+Coercion foo (n : nat) : Set.
+Admitted.
+Check (0 : Set).
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ee11d356d1..c76432ae3e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -463,8 +463,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
- 	  start_proof_and_print (local,p,DefinitionBody Definition)
-	    [Some (lid,pl), (bl,t,None)] no_hook
+	  start_proof_and_print (local,p,DefinitionBody k)
+	    [Some (lid,pl), (bl,t,None)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
-- 
cgit v1.2.3


From 780f3424fb741385f063864d9b15b2c3e3fc419a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 11:25:19 +0200
Subject: Fix bug #4705: coqtop accepts both -emacs and -ideslave.

---
 toplevel/coqtop.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cfedff0809..9e1a76bbd6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -241,11 +241,26 @@ let compile_files () =
 (** Options for proof general *)
 
 let set_emacs () =
+  if not (Option.is_empty !toploop) then
+    error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
   Pp.make_pp_emacs ();
   Vernacentries.qed_display_script := false;
   color := `OFF
 
+(** Options for CoqIDE *)
+
+let set_ideslave () =
+  if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible";
+  toploop := Some "coqidetop";
+  Flags.ide_slave := true
+
+(** Options for slaves *)
+
+let set_toploop name =
+  if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible";
+  toploop := Some name
+
 (** GC tweaking *)
 
 (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
@@ -501,7 +516,7 @@ let parse_args arglist =
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
-    |"-toploop" -> toploop := Some (next ())
+    |"-toploop" -> set_toploop (next ())
     |"-w" -> set_warning (next ())
 
     (* Options with zero arg *)
@@ -522,7 +537,7 @@ let parse_args arglist =
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
-    |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
+    |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-just-parsing" -> Vernac.just_parsing := true
-- 
cgit v1.2.3


From 443857fe1bbecf089eb40d522a71a014273c5a23 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 14:06:17 +0200
Subject: Use the canonical name when looking for an eliminator (bug #4670).

Disclaimer: I have no idea what I am doing.
---
 pretyping/indrec.ml           | 2 +-
 test-suite/bugs/closed/4670.v | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4670.v

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0588dcc87f..589b8d82ab 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -598,7 +598,7 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = repr_mind kn in
+  let mp,dp,l = KerName.repr (MutInd.canonical kn) in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 0000000000..6113992953
--- /dev/null
+++ b/test-suite/bugs/closed/4670.v
@@ -0,0 +1,7 @@
+Require Import Coq.Vectors.Vector.
+Module Bar.
+  Definition foo A n (l : Vector.t A n) : True.
+  Proof.
+    induction l ; exact I.
+  Defined.
+End Bar.
-- 
cgit v1.2.3


From e7d54d7fe751e21001c6873fc6092b5adc8eb682 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 14:22:04 +0200
Subject: Fix bug #4292: Unexpected functor objects.

---
 library/declaremods.ml        | 5 ++++-
 test-suite/bugs/closed/4292.v | 7 +++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4292.v

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0434841513..651c76ae17 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -727,7 +727,10 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   let arg_entries_r = intern_args interp_modast args in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let entry = params, fst (interp_modast env ModType mty) in
+  let mte, _ = interp_modast env ModType mty in
+  (* We check immediately that mte is well-formed *)
+  let _ = Mod_typing.translate_mse env None inl mte in
+  let entry = params, mte in
   let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
   let sobjs = get_functor_sobjs false env inl entry in
   let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
diff --git a/test-suite/bugs/closed/4292.v b/test-suite/bugs/closed/4292.v
new file mode 100644
index 0000000000..403e155eaf
--- /dev/null
+++ b/test-suite/bugs/closed/4292.v
@@ -0,0 +1,7 @@
+Module Type S. End S.
+
+Declare Module M : S.
+
+Module Type F (T: S). End F.
+
+Fail Module Type N := F with Module T := M.
-- 
cgit v1.2.3


From 00a13c3c014e2729d17ad8e8191f20586ae3b52b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 3 May 2016 15:50:13 +0200
Subject: Test file for #4695: Slow Qed.

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

diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 0000000000..a42271811d
--- /dev/null
+++ b/test-suite/bugs/closed/4695.v
@@ -0,0 +1,38 @@
+(* 
+The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel
+term comparison after evaluation was done on constants according to their user
+names. The conversion still succeeded because delta applied, but was much
+slower than with a canonical names comparison.
+*)
+
+Module Mod0.
+
+  Fixpoint rec_ t d : nat :=
+    match d with
+    | O => O
+    | S d' =>
+      match t with
+      | true => rec_ t d'
+      | false => rec_ t d'
+      end
+    end.
+
+  Definition depth := 1000.
+
+  Definition rec t := rec_ t depth.
+
+End Mod0.
+
+
+Module Mod1.
+  Module M := Mod0.
+End Mod1.
+
+
+Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n.
+
+Lemma slow_qed : forall t n,
+    Mod0.rec t = n.
+Proof.
+  intros; unfold Mod0.rec; apply rec_prop.
+Timeout 2 Qed.
-- 
cgit v1.2.3


From b6e796a8ef956fa25bfeba84545f25b2cfb3aaf9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 15:06:11 +0200
Subject: Fix bug #3825: Universe annotations on notations should pass through
 or be rejected.

---
 interp/constrintern.ml        | 10 +++++++++-
 test-suite/bugs/closed/3825.v | 16 ++++++++++++++++
 test-suite/bugs/closed/3922.v |  2 +-
 test-suite/bugs/closed/4544.v |  2 +-
 4 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/3825.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a7b1bb4128..ead68bd92f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -767,7 +767,15 @@ let intern_qualid loc qid intern env lvar us args =
       let subst = (terms, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
       let projapp = match c with NRef _ -> true | _ -> false in
-	subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2
+      let c = subst_aconstr_in_glob_constr loc intern lvar subst infos c in
+      let c = match us, c with
+      | None, _ -> c
+      | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+      | Some _, _ ->
+        user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
+          str " cannot have a universe instance")
+      in
+      c, projapp, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 0000000000..e594b74b62
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 5013bc6ac1..d88e8c3325 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -73,7 +73,7 @@ Definition Trunc_ind {n A}
   (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
   : (forall a, P (tr a)) -> (forall aa, P aa)
 := (fun f aa => match aa with tr a => fun _ => f a end Pt).
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
            (P : Type) `{Pc : X -> Contr P}
            (g : X -> P) (h : P -> Y) (p : h o g == f)
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc7..048f31ce3d 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -841,7 +841,7 @@ End Truncation_Modalities.
 
 Module Import TrM := Modalities_Theory Truncation_Modalities.
 
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 
 Notation IsSurjection := (IsConnMap -1).
 
-- 
cgit v1.2.3


From 29697585836c6e0e4d91e28a13c3f40d2137208b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 18:23:32 +0200
Subject: Fix bug #4707: clearbody much slower in 8.5pl1.

We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.
---
 tactics/tactics.ml | 56 ++++++++++++++++++++++++++++++++----------------------
 1 file changed, 33 insertions(+), 23 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28aed8a10e..63d3c694ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1789,17 +1789,17 @@ let on_the_bodies = function
 | [id] -> str " depends on the body of " ++ pr_id id
 | l -> str " depends on the bodies of " ++ pr_sequence pr_id l
 
-let check_is_type env ty msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
+exception DependsOnBody of Id.t option
+
+let check_is_type env sigma ty =
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    raise (DependsOnBody None)
 
-let check_decl env (_, c, ty) msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
+let check_decl env sigma (id, c, ty) =
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
@@ -1807,14 +1807,15 @@ let check_decl env (_, c, ty) msg =
     | None -> ()
     | Some c -> Typing.check env evdref c ty
     in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    raise (DependsOnBody (Some id))
 
 let clear_body ids =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let sigma = Proofview.Goal.sigma gl in
     let ctx = named_context env in
     let map (id, body, t as decl) = match body with
     | None ->
@@ -1828,23 +1829,32 @@ let clear_body ids =
     let ctx = List.map map ctx in
     let base_env = reset_context env in
     let env = push_named_context ctx base_env in
-    let check_hyps =
-      let check env (id, _, _ as decl) =
-        let msg _ = Tacticals.New.tclZEROMSG
-          (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids)
+    let check =
+      try
+        let check (env, sigma) decl =
+          (** Do no recheck hypotheses that do not depend *)
+          let sigma =
+            if List.exists (fun id -> occur_var_in_decl env id decl) ids then
+              check_decl env sigma decl
+            else sigma
+          in
+          (push_named decl env, sigma)
         in
-        check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env)
-      in
-      let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in
-      Proofview.tclIGNORE checks
-    in
-    let check_concl =
-      let msg _ = Tacticals.New.tclZEROMSG
-        (str "Conclusion" ++ on_the_bodies ids)
-      in
-      check_is_type env concl msg
+        let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in
+        let sigma =
+          if List.exists (fun id -> occur_var env id concl) ids then
+            check_is_type env sigma concl
+          else sigma
+        in
+        Proofview.Unsafe.tclEVARS sigma
+      with DependsOnBody where ->
+        let msg = match where with
+        | None -> str "Conclusion" ++ on_the_bodies ids
+        | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids
+        in
+        Tacticals.New.tclZEROMSG msg
     in
-    check_hyps <*> check_concl <*>
+    check <*>
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end
-- 
cgit v1.2.3


From 27689bac62f85c039517cbd003f8ea74cb9b4aa7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 24 Apr 2016 18:22:53 +0200
Subject: In Regular Subst Tactic mode, ensure that the order of hypotheses is
 preserved, which is a source of incompatibilities w.r.t. released 8.5 but
 which looks to me to be the only possible canonical behavior.

This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.

So, I consider this to be a fix to the "Regular Subst Tactic" mode.

Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
---
 CHANGES                     |  1 +
 doc/refman/RefMan-tac.tex   | 53 ++++++++++++++++---------
 tactics/equality.ml         | 35 ++++++++--------
 test-suite/output/subst.out | 97 +++++++++++++++++++++++++++++++++++++++++++++
 test-suite/output/subst.v   | 48 ++++++++++++++++++++++
 5 files changed, 198 insertions(+), 36 deletions(-)
 create mode 100644 test-suite/output/subst.out
 create mode 100644 test-suite/output/subst.v

diff --git a/CHANGES b/CHANGES
index 79fe3642b2..6a1f8f0e49 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,7 @@ Changes from V8.5pl1 to V8.5pl2
 Bugfixes
 
 - #4677: fix alpha-conversion in notations needing eta-expansion
+- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
 
 Changes from V8.5 to V8.5pl1
 ============================
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 903e2e19af..fa595d9159 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2854,42 +2854,57 @@ This tactic is deprecated. It can be replaced by {\tt enough}
 \tacindex{subst}
 \optindex{Regular Subst Tactic}
 
-This tactic applies to a goal that has \ident\ in its context and
-(at least) one hypothesis, say {\tt H}, of type {\tt
-  \ident=t} or {\tt t=\ident}. Then it replaces
-\ident\ by {\tt t} everywhere in the goal (in the hypotheses
-and in the conclusion) and clears \ident\ and {\tt H} from the context.
+This tactic applies to a goal that has \ident\ in its context and (at
+least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$
+{\tt = \ident} with {\ident} not occurring in $t$.  Then it replaces
+{\ident} by $t$ everywhere in the goal (in the hypotheses and in the
+conclusion) and clears {\ident} and $H$ from the context.
+
+If {\ident} is a local definition of the form {\ident} := $t$, it is
+also unfolded and cleared.
+
+\Rem
+When several hypotheses have the form {\tt \ident} = $t$ or {\tt
+  $t$ = \ident}, the first one is used.
 
 \Rem
-When several hypotheses have the form {\tt \ident=t} or {\tt
-  t=\ident}, the first one is used.
+If $H$ is itself dependent in the goal, it is replaced by the
+proof of reflexivity of equality.
 
 \begin{Variants}
-  \item {\tt subst \ident$_1$ \dots \ident$_n$}
+  \item {\tt subst \ident$_1$ {\dots} \ident$_n$}
 
-    Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
+    This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
   \item {\tt subst}
 
-    Applies {\tt subst} repeatedly to all identifiers from the context
-    for which an equality exists.
+    This applies {\tt subst} repeatedly from top to bottom to all
+    identifiers of the context for which an equality of the form {\tt
+      \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with
+    {\ident} not occurring in $t$.
 
-\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set
-    Regular Subst Tactic}. When this option is activated, {\tt subst}
-  manages the following corner cases which otherwise it
-  does not:
+\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled
+using option {\tt Set Regular Subst Tactic}. When this option is
+activated, {\tt subst} also deals with the following corner cases:
 \begin{itemize}
 \item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$}
   and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a
   variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$}
-  or {\tt $u$ = \ident$_2$}
+  or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt
+    subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$
+  respectively.
+
 \item A context with cyclic dependencies as with hypotheses {\tt
-  \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$}
+  \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which
+  without the option would be a cause of failure of {\tt subst}.
 \end{itemize}
-Additionally, it prevents a local definition such as {\tt \ident :=
-  $t$} to be unfolded which otherwise it would exceptionally unfold in
+Additionally, it prevents a local definition such as {\tt \ident} :=
+  $t$ to be unfolded which otherwise it would exceptionally unfold in
 configurations containing hypotheses of the form {\tt {\ident} = $u$},
 or {\tt $u'$ = \ident} with $u'$ not a variable.
 
+Finally, it preserves the initial order of hypotheses, which without
+the option it may break.
+
 The option is off by default.
 
 \end{Variants}
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f72a72f46d..819a995db1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1595,6 +1595,17 @@ user = raise user error specific to rewrite
 (**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
+let regular_subst_tactic = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "more regular behavior of tactic subst";
+      optkey   = ["Regular";"Subst";"Tactic"];
+      optread  = (fun () -> !regular_subst_tactic);
+      optwrite = (:=) regular_subst_tactic }
+
 let unfold_body x =
   Proofview.Goal.enter begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
@@ -1642,23 +1653,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
-    List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
+    List.rev (pi3 (List.fold_right (fun (id,b,_ as dcl) (dest,deps,allhyps) ->
       if not (Id.equal id hyp)
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
-        ((if b = None then deps else id::deps), id::allhyps)
+        let id_dest = if !regular_subst_tactic then dest else MoveLast in
+        (dest,(if b = None then deps else id::deps), (id_dest,id)::allhyps)
       else
-        (deps,allhyps))
+        (MoveBefore id,deps,allhyps))
       hyps
-      ([x],[]))) in
+      (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var env x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [revert dephyps;
+      [revert (List.map snd dephyps);
        general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
-       (tclMAP intro_using dephyps)]
+       (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
@@ -1709,17 +1721,6 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
-let regular_subst_tactic = ref false
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "more regular behavior of tactic subst";
-      optkey   = ["Regular";"Subst";"Tactic"];
-      optread  = (fun () -> !regular_subst_tactic);
-      optwrite = (:=) regular_subst_tactic }
-
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
   if !regular_subst_tactic then
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 0000000000..f5768ba441
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+   True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+   True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+   True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+   True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  HA, HB : True
+  H4 : 0 = 4
+  H3 : 0 = 3
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+   True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 0000000000..e48aa6bb28
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+
-- 
cgit v1.2.3


From 9173d3b0c4127e8217e93f8aad8ccba94037b486 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 May 2016 08:48:30 +0200
Subject: Increase the size of the dumpglob buffer for cooking notations (bug
 #4708).

A single terminal character can take up to 5 bytes, e.g. "''^A'".
---
 interp/dumpglob.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 44a62ef379..85212b7aba 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -172,7 +172,7 @@ let cook_notation df sc =
   (* - all single quotes in terminal tokens are doubled                       *)
   (* - characters < 32 are represented by '^A, '^B, '^C, etc                  *)
   (* The output is decoded in function Index.prepare_entry of coqdoc          *)
-  let ntn = String.make (String.length df * 3) '_' in
+  let ntn = String.make (String.length df * 5) '_' in
   let j = ref 0 in
   let l = String.length df - 1 in
   let i = ref 0 in
-- 
cgit v1.2.3


From 1dd8d826592507046b35128800578149021dab4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 2 May 2016 17:11:22 +0200
Subject: Fix for #4603, part 3: definitions inside proofs not handled properly
 by coqc.

Patch by Matthieu, Enrico and myself.
---
 stm/stm.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index bec9d18d51..95cecb7fe2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1839,7 +1839,7 @@ let known_state ?(redefine_qed=false) ~cache id =
             if ctac then Hooks.(call tactic_being_run true); 
             vernac_interp id x;
             if ctac then Hooks.(call tactic_being_run false); 
-	    if eff then update_global_env ()), cache, true
+	    if eff then update_global_env ()), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
@@ -2247,13 +2247,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           vernac_interp (VCS.get_branch_pos head) x; `Ok
 
       | VtSideff l, w ->
+	  let ceff_in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
 	  let replay = match x.expr with
 	    | VernacDefinition(_, _, DefineBody _) -> None
 	    | _ -> Some x
 	  in
+          VCS.commit id (Cmd {ctac=false;ceff=ceff_in_proof;cast=x;cids=l;cqueue=`MainQueue});
 	  VCS.propagate_sideff replay;
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
-- 
cgit v1.2.3


From dd7cf3a8086fa8a08a421314caec8543ba62226b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 May 2016 10:36:43 +0200
Subject: Handle primitive projections inside types when extracting (bug
 #4616).

Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
---
 plugins/extraction/extraction.ml | 2 +-
 test-suite/bugs/closed/4616.v    | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4616.v

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 10644da25d..667721e670 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -285,7 +285,7 @@ let rec extract_type env db j c args =
     | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
-    | Case _ | Fix _ | CoFix _ -> Tunknown
+    | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown
     | _ -> assert false
 
 (*s Auxiliary function dealing with type application.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
new file mode 100644
index 0000000000..c862f82067
--- /dev/null
+++ b/test-suite/bugs/closed/4616.v
@@ -0,0 +1,4 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : Type }.
+Axiom f : forall t : Foo', foo t.
+Extraction f.
-- 
cgit v1.2.3


From 78e616d56dc0646d0c67ab57e11671a6c08d0cc7 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Mon, 8 Feb 2016 16:08:10 -0500
Subject: Fix Haskell extraction for terms over 45 characters long

The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name.  In particular, with a term
name of 46 characters or more, the following Coq code:

  Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
  Extraction Language Haskell.
  Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.

would produce:

  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
  Unit
  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
    Tt

which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).

This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
---
 plugins/extraction/haskell.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 22519e3471..764223621e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -346,7 +346,7 @@ let pp_decl = function
 	  in
 	  if void then mt ()
 	  else
-	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
+	    hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++
 	    (if is_custom r then
 		(names.(i) ++ str " = " ++ str (find_custom r))
 	     else
@@ -357,7 +357,7 @@ let pp_decl = function
       if is_inline_custom r then mt ()
       else
 	let e = pp_global Term r in
-	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+	hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++
 	  if is_custom r then
 	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
 	  else
-- 
cgit v1.2.3


From 796859aca4fc85dc721b670d95b0c2aaace55e32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 May 2016 11:15:37 +0200
Subject: Fixing subst.out after changing spacing in goal output (24a125b77).

---
 test-suite/output/subst.out | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index f5768ba441..209b2bc26f 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -10,7 +10,7 @@
   HB : True
   H4 : z = 4
   ============================
-   True
+  True
 1 subgoal
   
   x, z : nat
@@ -23,7 +23,7 @@
   HB : True
   H4 : z = 4
   ============================
-   True
+  True
 1 subgoal
   
   x, y : nat
@@ -36,7 +36,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   H1 : 0 = 1
@@ -46,7 +46,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   y, z : nat
@@ -59,7 +59,7 @@
   H1 : 0 = 1
   H2 : 0 = 2
   ============================
-   True
+  True
 1 subgoal
   
   x, z : nat
@@ -72,7 +72,7 @@
   H4 : z = 4
   H3 : 0 = 3
   ============================
-   True
+  True
 1 subgoal
   
   x, y : nat
@@ -85,7 +85,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   HA, HB : True
@@ -94,4 +94,4 @@
   H1 : 0 = 1
   H2 : 0 = 2
   ============================
-   True
+  True
-- 
cgit v1.2.3


From 174fd1f853f47d24b350a53e7f186ab37829dc2a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 4 May 2016 12:08:30 +0200
Subject: Int.v: simplify Jason's commit 5b4e3ace

---
 theories/ZArith/Int.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index b78891c711..143d3c8dbe 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -452,7 +452,7 @@ Module Z_as_Int <: Int.
   Proof. reflexivity. Qed.
 
   (** Compatibility notations for Coq v8.4 *)
-  Notation plus := Coq.ZArith.Int.Z_as_Int.add (compat "8.4").
-  Notation minus := Coq.ZArith.Int.Z_as_Int.sub (compat "8.4").
-  Notation mult := Coq.ZArith.Int.Z_as_Int.mul (compat "8.4").
+  Notation plus := add (compat "8.4").
+  Notation minus := sub (compat "8.4").
+  Notation mult := mul (compat "8.4").
 End Z_as_Int.
-- 
cgit v1.2.3