From b3d372c410e3dfffe5183632d1fe17917a829b9a Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Wed, 7 Sep 2016 15:17:29 -0700
Subject: Fix a typo in the reference manual

---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9fbff7181..1d89c17f4 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1158,7 +1158,7 @@ using the syntax:
 \end{quote}
 A previous definition of {\qualid} must exist in the environment.
 The new definition will always be used instead of the old one and
-it goes accross module boundaries.
+it goes across module boundaries.
 
 If preceded by the keyword {\tt Local} the tactic definition will not
 be exported outside the current module.
-- 
cgit v1.2.3


From 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf Mon Sep 17 00:00:00 2001
From: Frédéric Besson <frederic.besson@inria.fr>
Date: Thu, 8 Sep 2016 14:19:02 +0200
Subject: Fix Bug #5073 : regression of micromega plugin

The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
---
 plugins/micromega/coq_micromega.ml | 24 +++++++++++++++---------
 plugins/micromega/mutils.ml        | 12 ------------
 test-suite/micromega/zomicron.v    |  7 +++++++
 3 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db8cbf231..23d37c273 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -961,7 +961,7 @@ struct
           let (env,n) = _add l ( n+1) v in
            (e::env,n) in
     let (env, n) =  _add env 1 v in
-     (env, CamlToCoq.idx n)
+     (env, CamlToCoq.positive n)
 
    let get_rank env v = 
 
@@ -1986,21 +1986,27 @@ let micromega_gen
                                                     micromega_order_change spec res'
                                                       (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in
 
+       let goal_props = List.rev (prop_env_of_formula ff') in 
+
+       let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in 
+       
+       let arith_args = goal_props @ goal_vars in
+
        let kill_arith = 
            Tacticals.New.tclTHEN
              (Tactics.keep [])
              ((*Tactics.tclABSTRACT  None*)
                 (Tacticals.New.tclTHEN tac_arith tac)) in 
 
-       Tacticals.New.tclTHEN
-         (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal)
-         (Tacticals.New.tclTHENLIST
+       Tacticals.New.tclTHENS
+         (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+         [
+           kill_arith;
+           (Tacticals.New.tclTHENLIST
             [(Tactics.generalize (List.map Term.mkVar ids));
-                Tactics.unfold_constr coq_not_gl_ref;
-                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
-            ])
-                (*Tacticals.New.tclTRY(Tactics.apply_with_bindings_gen true false
-                  [None,(Loc.ghost,((Term.mkVar goal_name) ,Misctypes.NoBindings))]*)
+             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            ] )
+         ]
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
     | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index c13e8fc28..b4c6d032b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -294,18 +294,6 @@ struct
   else  XO (index (n lsr 1))
 
 
- let idx n =
-  (*a.k.a path_of_int *)
-  (* returns the list of digits of n in reverse order with initial 1 removed *)
-  let rec digits_of_int n =
-   if Int.equal n 1 then []
-   else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
-  in
-   List.fold_right
-    (fun b c -> (if b then XI c else XO c))
-    (List.rev (digits_of_int n))
-    (XH)
-
  let z x =
   match compare x 0 with
    | 0 -> Z0
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 3f4c2407d..239bc6936 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -82,4 +82,11 @@ Proof.
   lia.
 Qed.
 
+(*  Bug 5073 *)
+Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+Proof.
+  lia.
+Qed.
+
+
 
-- 
cgit v1.2.3


From ef3f9fac7cff820bd927d122caef2c37a68a55c8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 8 Sep 2016 17:04:43 +0200
Subject: Avoid canonizing the same paths over and over.

The number of path canonizations was quadratic in the number of potential
plugin directories. This patch makes it linear; on a standard Coq tree,
this brings the number of chdir and getcwd system calls from more than
1,000 down to about 200 at startup.

This also fixes a bug where the Cd vernacular command could cause plugins
to break since relative paths were used to locate them.
---
 toplevel/mltop.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fbd1e6033..f97295945 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -45,12 +45,12 @@ open System
    to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *)
 
 (* This path is where we look for .cmo *)
-let coq_mlpath_copy = ref ["."]
+let coq_mlpath_copy = ref [Sys.getcwd ()]
 let keep_copy_mlpath path =
   let cpath = CUnix.canonical_path_name path in
-  let filter path' = not (String.equal cpath (CUnix.canonical_path_name path'))
+  let filter path' = not (String.equal cpath path')
   in
-  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
+  coq_mlpath_copy := cpath :: List.filter filter !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = {
-- 
cgit v1.2.3


From e65c629bac48e61b3a14f05bfafc6b85486359c0 Mon Sep 17 00:00:00 2001
From: Frédéric Besson <frederic.besson@inria.fr>
Date: Thu, 8 Sep 2016 23:23:36 +0200
Subject: Fix Bug #5073 : regression of micromega plugin

esprit d'escalier : is now also fixed for R
---
 plugins/micromega/coq_micromega.ml | 35 ++++++++++++++++++++---------------
 test-suite/micromega/rexample.v    |  5 +++++
 2 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 23d37c273..a063cbbfe 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2100,22 +2100,27 @@ let micromega_genr prover tac =
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
                                                     micromega_order_changer res' env' ff_arith ] in
 
+       let goal_props = List.rev (prop_env_of_formula ff') in 
+
+       let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in 
+       
+       let arith_args = goal_props @ goal_vars in
+
        let kill_arith = 
-         Tacticals.New.tclTHEN
-           (Tactics.keep [])
-           ((*Tactics.tclABSTRACT  None*)
-             (Tacticals.New.tclTHEN tac_arith tac)) in 
-
-
-       Tacticals.New.tclTHEN
-         (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal)
-        
-         (Tacticals.New.tclTHENLIST
-               [(Tactics.generalize (List.map Term.mkVar ids));
-                Tactics.unfold_constr coq_not_gl_ref;
-                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
-               ]
-         )
+           Tacticals.New.tclTHEN
+             (Tactics.keep [])
+             ((*Tactics.tclABSTRACT  None*)
+                (Tacticals.New.tclTHEN tac_arith tac)) in 
+
+       Tacticals.New.tclTHENS
+         (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+         [
+           kill_arith;
+           (Tacticals.New.tclTHENLIST
+            [(Tactics.generalize (List.map Term.mkVar ids));
+             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            ] )
+         ]
 
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 12f72a580..bd5227010 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -81,3 +81,8 @@ Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; lra.
 Qed.
 
+(*  Bug 5073 *)
+Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+Proof.
+  lra.
+Qed.
-- 
cgit v1.2.3


From 5ecd8a6a5593d7f197a115b129ebd5f530e40161 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 8 Sep 2016 23:44:44 +0200
Subject: Fix bug #3920 for good after 44ada64.

The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
---
 ltac/rewrite.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index cf59b6dc1..69f45e1ae 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1578,11 +1578,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	| Some id, Some p ->
             let tac = tclTHENLIST [
               Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
-              beta_hyp id;
               Proofview.Unsafe.tclNEWGOALS gls;
             ] in
             Proofview.Unsafe.tclEVARS undef <*>
-	    assert_replacing id newt tac
+	    tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
             convert_hyp_no_check (LocalAssum (id, newt)) <*>
-- 
cgit v1.2.3


From 01d0c1224e0a29f10b2cef5b3fd2b4d06a686055 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 9 Sep 2016 11:30:41 +0200
Subject: Update csdp cache.

This was making the test-suite fail on machines where csdp was not installed.
---
 test-suite/.csdp.cache | Bin 79491 -> 89077 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index 75dd38fde..b8c07512f 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
-- 
cgit v1.2.3


From dee69387bd4b2944c9e81ee422fb9900ab0e6c4d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 9 Sep 2016 11:34:22 +0200
Subject: Make it explicit when paths are added to the ML search paths.

When Mltop.add_rec_path was called to add paths to the loadpath, it was
also adding the top directory to the mlpath. In particular, "theories" was
added to the mlpath although it was explicitly marked "~with_ml:false".

The "plugins" and "user-contribs" subdirectories were scanned twice, once
for filling the loadpath and then for filling the mlpath.

This patch adds an argument to Mltop.add_rec_path to explicitly control
which paths from the loadpath are added to the mlpath (none, the top one,
all of them). The "top" option was the single old behavior; the "none"
option is used for "theories"; the "all" option is used to avoid
duplicate scanning for "plugins" and "user-contribs".
---
 toplevel/coqinit.ml       | 11 +++++------
 toplevel/mltop.ml         |  9 +++++++--
 toplevel/mltop.mli        |  4 +++-
 toplevel/vernacentries.ml |  2 +-
 4 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d9cd574a0..258a1135f 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,13 +59,12 @@ let load_rcfile() =
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
-  Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init);
-  if with_ml then
-    Mltop.add_rec_ml_dir unix_path
+  let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
+  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init)
 
 let add_userlib_path ~unix_path =
-  Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
-  Mltop.add_rec_ml_dir unix_path
+  Mltop.add_rec_path Mltop.AddRecML ~unix_path
+    ~coq_root:Nameops.default_root_prefix ~implicit:false
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
@@ -108,7 +107,7 @@ let init_load_path () =
     (* additional loadpath, given with options -Q and -R *)
     List.iter
       (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path ~unix_path ~coq_root ~implicit)
+        Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index f97295945..0a5b92270 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -182,7 +182,9 @@ let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
       (fun unix_path -> str "Cannot open " ++ str unix_path)
 
-let add_rec_path ~unix_path ~coq_root ~implicit =
+type add_ml = AddNoML | AddTopML | AddRecML
+
+let add_rec_path add_ml ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = Names.DirPath.repr coq_root in
@@ -193,7 +195,10 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = add_ml_dir unix_path in
+    let () = match add_ml with
+      | AddNoML -> ()
+      | AddTopML -> add_ml_dir unix_path
+      | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
     let add (path, dir) =
       Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 5d0546824..6633cb937 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -46,8 +46,10 @@ val dir_ml_use : string -> unit
 val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
+type add_ml = AddNoML | AddTopML | AddRecML
+
 (** Adds a path to the Coq and ML paths *)
-val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
+val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33a8609a7..48a85b709 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -880,7 +880,7 @@ let expand filename =
 let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
   let alias = Option.default Nameops.default_root_prefix ldiropt in
-  Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit
+  Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
-- 
cgit v1.2.3


From 7a037b8c1de11b18d47b01e5b0262090f32bfc40 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 9 Sep 2016 13:00:02 +0200
Subject: Restore native compiler optimizations after they were broken by
 9e2ee58.

The greatest danger of OCaml's polymorphic equality is that PMP can
replace it with pointer equality at any time, be warned :)

The lack of optimization may account for an exponential blow-up in size
of the generated code, as well as worse runtime performance.
---
 kernel/nativecode.ml | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2159a702c..096aa7066 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -22,8 +22,12 @@ to OCaml code. *)
 
 (** Local names **)
 
+(* The first component is there for debugging purposes only *)
 type lname = { lname : name; luid : int }
 
+let eq_lname ln1 ln2 =
+  Int.equal ln1.luid ln2.luid
+
 let dummy_lname = { lname = Anonymous; luid = -1 }
 
 module LNord = 
@@ -82,6 +86,9 @@ let eq_gname gn1 gn2 =
   | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
   | _ -> false
 
+let dummy_gname =
+  Grel 0
+
 open Hashset.Combine
 
 let gname_hash gn = match gn with
@@ -404,9 +411,13 @@ let opush_lnames n env lns =
 let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
   match t1, t2 with
   | MLlocal ln1, MLlocal ln2 ->
+     (try
       Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2)
+     with Not_found ->
+      eq_lname ln1 ln2)
   | MLglobal gn1', MLglobal gn2' ->
       eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2')
+      || (eq_gname gn1 gn2' && eq_gname gn2 gn1')
   | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2
   | MLlam (lns1, ml1), MLlam (lns2, ml2) ->
       Int.equal (Array.length lns1) (Array.length lns2) &&
@@ -719,6 +730,11 @@ let push_global_norm gn params body =
 let push_global_case gn params annot a accu bs =
   push_global gn (Gletcase (gn, params, annot, a, accu, bs))
 
+(* Compares [t1] and [t2] up to alpha-equivalence. [t1] and [t2] may contain
+   free variables. *)
+let eq_mllambda t1 t2 =
+  eq_mllambda dummy_gname dummy_gname 0 LNmap.empty LNmap.empty t1 t2
+
 (*s Compilation environment *)
 
 type env =
@@ -897,9 +913,7 @@ let rec insert cargs body rl =
      let params = rm_params fv params in
      rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
  | Rcons(l,fv,body',rl) ->
-    (** ppedrot: It seems we only want to factorize common branches. It should
-        not matter to do so with a subapproximation by (==). *)
-     if body == body' then
+     if eq_mllambda body body' then
        let (c,params) = cargs in
        let params = rm_params fv params in
        l := (c,params)::!l
@@ -1446,12 +1460,14 @@ let optimize gdef l =
 
 	end
     | MLif(t,b1,b2) ->
+       (* This optimization is critical: it applies to all fixpoints that start
+       by matching on their recursive argument *)
 	let t = optimize s t in
 	let b1 = optimize s b1 in
 	let b2 = optimize s b2 in
 	begin match t, b2 with
 	| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
-	    when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *)
+	    when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
         | _, _ -> MLif(t, b1, b2)
 	end
     | MLmatch(annot,a,accu,bs) ->
-- 
cgit v1.2.3


From 0d3c319336efaee78fb799c44806d3b9b8b28a50 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 9 Sep 2016 15:03:50 +0200
Subject: Fix bug #4940: Tactic notation printing could be more informative.

---
 printing/pptactic.ml | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 917a277c9..e2c78a507 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -373,20 +373,25 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
+  let rec pr_user_symbol = function
+  | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+  | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+  | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
+  | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
+  | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
+  | Extend.Uentry tag ->
+    let ArgT.Any tag = tag in
+    ArgT.repr tag
+  | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+
   let pr_alias_key key =
     try
       let prods = (KNmap.find key !prnotation_tab).pptac_prods in
-      (* First printing strategy: only the head symbol *)
-      match prods with
-      | TacTerm s :: prods -> str s
-      | _ ->
-      (* Second printing strategy; if ever Tactic Notation is eventually *)
-      (* accepting notations not starting with an identifier *)
       let rec pr = function
-      | [] -> []
-      | TacTerm s :: prods -> s :: pr prods
-      | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
-      str (String.concat " " (pr prods))
+      | TacTerm s -> primitive s
+      | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+      in
+      pr_sequence pr prods
     with Not_found ->
       KerName.print key
 
-- 
cgit v1.2.3


From 306dfe775009681e492a2a59e3dcdc5b67bd9d73 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 9 Sep 2016 15:45:29 +0200
Subject: Monomorphize a costly boolean equality operation.

---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9ea..4ae72a515 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -501,7 +501,7 @@ let is_resolvable evi =
   Option.is_empty (Store.get evi.evar_extra resolvable)
 
 let mark_resolvability_undef b evi =
-  if is_resolvable evi = b then evi
+  if is_resolvable evi == (b : bool) then evi
   else
     let t = set_resolvable evi.evar_extra b in
     { evi with evar_extra = t }
-- 
cgit v1.2.3


From ff980722521812d19bc1e25cd504567b4a6b549a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 9 Sep 2016 16:37:35 +0200
Subject: Fast path in Clenvtac.clenv_refine typeclass resolution.

This legacy function is still used by destruct, and is a hotspot in various
examples from the wild. We hijack the check from Typeclass and perform a
double check at once not to mark unresolvable evars in vain a lot.
---
 pretyping/typeclasses.ml  |  4 ++--
 pretyping/typeclasses.mli |  2 +-
 proofs/clenvtac.ml        | 26 +++++++++++++++++++++++---
 3 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4ae72a515..31ef3dfdd 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -548,7 +548,7 @@ let solve_all_instances env evd filter unique split fail =
 (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
 (* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
 
-let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =
-  if not (has_typeclasses filter evd) then evd
+  if fast_path && not (has_typeclasses filter evd) then evd
   else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 25460ef7d..2530f5dfa 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -101,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info
 val is_class_evar : evar_map -> evar_info -> bool
 val is_class_type : evar_map -> types -> bool
 
-val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> 
+val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
 val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 04a2eb487..98b5bc8b0 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,6 +59,19 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
+(** Use our own fast path, more informative than from Typeclasses *)
+let check_tc evd =
+  let has_resolvable = ref false in
+  let check _ evi =
+    let res = Typeclasses.is_resolvable evi in
+    if res then
+      let () = has_resolvable := true in
+      Typeclasses.is_class_evar evd evi
+    else false
+  in
+  let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
+  (has_typeclass, !has_resolvable)
+
 let clenv_refine with_evars ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
@@ -67,9 +80,16 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
-      let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
-        ~fail:(not with_evars) clenv.env clenv.evd
-      in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+      let (has_typeclass, has_resolvable) = check_tc clenv.evd in
+      let evd' =
+        if has_typeclass then
+          Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+          ~fail:(not with_evars) clenv.env clenv.evd
+        else clenv.evd
+      in
+      if has_resolvable then
+        Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+      else evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
-- 
cgit v1.2.3


From a9efa6f9e601cc2bfa1968dca1cdc0d01ebf55e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 9 Sep 2016 17:09:59 +0200
Subject: Fix output test-suite after commit 0d3c319.

---
 test-suite/output/Errors.out |  2 +-
 test-suite/output/ltac.out   | 17 +++++++++++------
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 62e9ef4b2..06a6b2d15 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -6,5 +6,5 @@ The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
-Ltac call to "instantiate" failed.
+Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21554e9ff..f4254e4e2 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -4,20 +4,25 @@ Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z
 The command has indeed failed with message:
-In nested Ltac calls to "g1" and "refine", last call failed.
+In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f1" and "refine", last call failed.
+In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.
-- 
cgit v1.2.3


From 43869b4e05824244e666c60e0b740a80e8b09d0c Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Tue, 28 Jun 2016 12:37:00 -0400
Subject: no-refold patch

Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
---
 pretyping/evarconv.ml         |  8 ++--
 pretyping/reductionops.ml     | 86 +++++++++++++++++++++++++++++--------------
 pretyping/reductionops.mli    |  9 ++++-
 pretyping/unification.ml      |  7 ++--
 proofs/redexpr.ml             |  2 +-
 test-suite/bugs/closed/3424.v |  1 +
 test-suite/output/inference.v |  1 +
 theories/Compat/Coq85.v       |  3 +-
 8 files changed, 79 insertions(+), 38 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fea2ba22..b033f5a39 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -314,7 +314,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
   if Reductionops.Stack.compare_shape sk1 sk2 then
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
-    
+
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -432,7 +432,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       else quick_fail i
     and delta i =
       switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
-	(whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM))
+	     (whd_betaiota_deltazeta_for_iota_state
+  	        (fst ts) env i cstsM (vM,skM))
     in    
     let default i = ise_try i [f1; consume apprF apprM; delta]
     in
@@ -449,7 +450,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		try 
 		  let termM' = Retyping.expand_projection env evd p c [] in
 		  let apprM', cstsM' = 
-		    whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (termM',skM)
+		    whd_betaiota_deltazeta_for_iota_state
+		      (fst ts) env evd cstsM (termM',skM)
 		  in
 		  let delta' i = 
 		    switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8259876c2..4ccbc81b4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -26,6 +26,19 @@ exception Elimconst
     their parameters in its stack.
 *)
 
+let refolding_in_reduction = ref false
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Perform refolding of fixpoints/constants like cbn during reductions";
+  Goptions.optkey = ["Refolding";"Reduction"];
+  Goptions.optread = (fun () -> !refolding_in_reduction);
+  Goptions.optwrite = (fun a -> refolding_in_reduction:=a);
+}
+
+let get_refolding_in_reduction () = !refolding_in_reduction
+let set_refolding_in_reduction = (:=) refolding_in_reduction
+
 (** Machinery to custom the behavior of the reduction *)
 module ReductionBehaviour = struct
   open Globnames
@@ -623,16 +636,17 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
 
 (* Beta Reduction tools *)
 
-let apply_subst recfun env cst_l t stack =
+let apply_subst recfun env refold cst_l t stack =
   let rec aux env cst_l t stack =
     match (Stack.decomp stack,kind_of_term t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
-      aux (h::env) (Cst_stack.add_param h cst_l) c stacktl
+       let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
+       aux (h::env) cst_l' c stacktl
     | _ -> recfun cst_l (substl env t, stack)
   in aux env cst_l t stack
 
 let stacklam recfun env t stack =
-  apply_subst (fun _ -> recfun) env Cst_stack.empty t stack
+  apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack
 
 let beta_applist (c,l) =
   stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
@@ -697,11 +711,16 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
   substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env cst_l cofix sk =
-  let raw_answer = contract_cofix ~env ?reference:(Cst_stack.reference cst_l) cofix in
+let reduce_and_refold_cofix recfun env refold cst_l cofix sk =
+  let raw_answer =
+    let env = if refold then Some env else None in
+    contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
   apply_subst
-    (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk'))
-    [] Cst_stack.empty raw_answer sk
+    (fun x (t,sk') ->
+      let t' =
+        if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in
+      recfun x (t',sk'))
+    [] refold Cst_stack.empty raw_answer sk
 
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
@@ -737,11 +756,18 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env cst_l fix sk =
-  let raw_answer = contract_fix ~env ?reference:(Cst_stack.reference cst_l) fix in
+let reduce_and_refold_fix recfun env refold cst_l fix sk =
+  let raw_answer =
+    let env = if refold then None else Some env in
+    contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
   apply_subst
-    (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk'))
-    [] Cst_stack.empty raw_answer sk
+    (fun x (t,sk') ->
+      let t' =
+        if refold then
+          Cst_stack.best_replace (mkFix fix) cst_l t
+        else t
+      in recfun x (t',sk'))
+    [] refold Cst_stack.empty raw_answer sk
 
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum && bodynum < Array.length recindices);
@@ -781,7 +807,7 @@ let equal_stacks (x, l) (y, l') =
     | None -> false
     | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) 
 
-let rec whd_state_gen ?csts tactic_mode flags env sigma =
+let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec cst_l (x, stack as s) =
     let () = if !debug_RAKAM then
@@ -804,7 +830,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
-      | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
+      | LocalDef (_,body,_) ->
+	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
       | _ -> fold ())
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -819,7 +846,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	| None -> fold ()
 	| Some body ->
 	   if not tactic_mode
-	   then whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
+	   then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+		      (body, stack)
 	   else (* Looks for ReductionBehaviour *)
 	     match ReductionBehaviour.get (Globnames.ConstRef c) with
 	     | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
@@ -896,20 +924,20 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 				      Stack.append_app [|c|] bef,cst_l)::s'))
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
-      apply_subst whrec [b] cst_l c stack
+      apply_subst whrec [b] refold cst_l c stack
     | Cast (c,_,_) -> whrec cst_l (c, stack)
     | App (f,cl)  ->
       whrec
-	(Cst_stack.add_args cl cst_l)
+	(if refold then Cst_stack.add_args cl cst_l else cst_l)
 	(f, Stack.append_app cl stack)
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
-	apply_subst whrec [] cst_l x stack
+	apply_subst whrec [] refold cst_l x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
 	let env' = push_rel (LocalAssum (na,t)) env in
-	let whrec' = whd_state_gen tactic_mode flags env' sigma in
-        (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with
+	let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
+        (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
 	  if napp > 0 then
@@ -945,7 +973,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
 	  let x' = Stack.zip(x,args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
-	  reduce_and_refold_fix whrec env cst_l f out_sk
+	  reduce_and_refold_fix whrec env refold cst_l f out_sk
 	|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
 	  let x' = Stack.zip(x,args) in
 	  begin match remains with
@@ -955,7 +983,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	      (match constant_opt_value_in env const with
 	      | None -> fold ()
 	      | Some body ->
-		whrec (Cst_stack.add_cst (mkConstU const) cst_l)
+		whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		  (body, s' @ (Stack.append_app [|x'|] s'')))
 	    | Stack.Cst_proj p ->
 	      let pb = lookup_projection p env in
@@ -981,7 +1009,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
-	  reduce_and_refold_cofix whrec env cst_l cofix stack
+	  reduce_and_refold_cofix whrec env refold cst_l cofix stack
 	|_ -> fold ()
       else fold ()
 
@@ -1073,7 +1101,7 @@ let local_whd_state_gen flags sigma =
   whrec
 
 let raw_whd_state_gen flags env =
-  let f sigma s = fst (whd_state_gen false flags env sigma s) in
+  let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
   f
 
 let stack_red_of_state_red f =
@@ -1083,7 +1111,7 @@ let stack_red_of_state_red f =
 (* Drops the Cst_stack *)
 let iterate_whd_gen refold flags env sigma s =
   let rec aux t =
-  let (hd,sk),_ = whd_state_gen refold flags env sigma (t,Stack.empty) in
+  let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
   Stack.zip ~refold (hd,whd_sk)
   in aux s
@@ -1468,19 +1496,21 @@ let is_sort env sigma t =
    of case/fix (heuristic used by evar_conv) *)
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+  let refold = get_refolding_in_reduction () in
+  let tactic_mode = false in
   let rec whrec csts s =
-    let (t, stack as s),csts' = whd_state_gen ~csts false CClosure.betaiota env sigma s in
+    let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
-	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Fix _ :: _ as stack') ->
-	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Proj (n,m,p,_) :: stack'') ->
-	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 874ea6815..4cd7a2a86 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -28,6 +28,11 @@ module ReductionBehaviour : sig
   val print : Globnames.global_reference -> Pp.std_ppcmds
 end
 
+(** Option telling if reduction should use the refolding machinery of cbn
+   (off by default) *)
+val get_refolding_in_reduction : unit -> bool
+val set_refolding_in_reduction : bool -> unit
+
 (** {6 Machinery about a stack of unfolded constant }
 
     cst applied to params must convertible to term of the state applied to args
@@ -134,8 +139,8 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
 
-val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
+val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
+  CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
 
 val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6d80db645..bc888b897 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -479,8 +479,8 @@ let unfold_projection env p stk =
 let expand_key ts env sigma = function
   | Some (IsKey k) -> expand_table_key env k
   | Some (IsProj (p, c)) -> 
-    let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma 
-				Cst_stack.empty (c, unfold_projection env p [])))
+    let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
+                               Cst_stack.empty (c, unfold_projection env p [])))
     in if Term.eq_constr (mkProj (p, c)) red then None else Some red
   | None -> None
 
@@ -572,7 +572,8 @@ let constr_cmp pb sigma flags t u =
     else sigma, b
     
 let do_reduce ts (env, nb) sigma c =
-  Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty)))
+  Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
+		  ts env sigma Cst_stack.empty (c, Stack.empty)))
 
 let use_full_betaiota flags =
   flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8a9ce4f94..72cb05f1b 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -44,7 +44,7 @@ let cbv_native env sigma c =
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
   in Reductionops.Stack.zip ~refold:true state
 
 let strong_cbn flags =
diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v
index f9b2c3861..ee8cabf17 100644
--- a/test-suite/bugs/closed/3424.v
+++ b/test-suite/bugs/closed/3424.v
@@ -13,6 +13,7 @@ Notation "0" := (trunc_S minus_one) : trunc_scope.
 Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
 Notation IsHProp := (IsTrunc minus_one).
 Notation IsHSet := (IsTrunc 0).
+Set Refolding Reduction.
 Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }.
 Proof.
 intros.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12b..1825db167 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 
 
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 54621cc1c..0ddf1acde 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -20,4 +20,5 @@ Global Unset Bracketing Last Introduction Pattern.
 Global Unset Regular Subst Tactic.
 Global Unset Structural Injection.
 Global Unset Shrink Abstract.
-Global Unset Shrink Obligations.
\ No newline at end of file
+Global Unset Shrink Obligations.
+Global Set Refolding Reduction.
\ No newline at end of file
-- 
cgit v1.2.3


From cc08fd749889b64dd219673efa4eebc3be6d956a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 1 Sep 2016 17:41:29 +0200
Subject: Updating .gitignore.

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 8a0c54f8f..4acd9930e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -54,6 +54,7 @@ kernel/byterun/dllcoqrun.so
 coqdoc.sty
 csdp.cache
 test-suite/lia.cache
+test-suite/nra.cache
 test-suite/trace
 test-suite/misc/universes/all_stdlib.v
 test-suite/misc/universes/universes.txt
-- 
cgit v1.2.3


From 43104a0b94e42fb78764b5d1365ca1e85a158508 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 10 Sep 2016 11:31:01 +0200
Subject: Fixing #5077 (failure on typing a fixpoint with evars in its type).

Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
---
 pretyping/pretyping.ml | 17 +----------------
 pretyping/typing.ml    | 12 +++++++++++-
 pretyping/typing.mli   |  5 +++++
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d6f8f0de5..2e164e540 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -267,21 +267,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
 (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
-(* Utilisé pour inférer le prédicat des Cases *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
-
-let evar_type_fixpoint loc env evdref lna lar vdefj =
-  let lt = Array.length vdefj in
-    if Int.equal (Array.length lar) lt then
-      for i = 0 to lt-1 do
-        if not (e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env !evdref
-            i lna vdefj lar
-      done
-
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
   | None -> j
@@ -579,7 +564,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      evar_type_fixpoint loc env evdref names ftys vdefj;
+      Typing.check_type_fixpoint loc env evdref names ftys vdefj;
       let ftys = Array.map (nf_evar !evdref) ftys in
       let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
       let fixj = match fixkind with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index eb16628b1..bb3f19859 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj =
   { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
+let check_type_fixpoint loc env evdref lna lar vdefj =
+  let lt = Array.length vdefj in
+    if Int.equal (Array.length lar) lt then
+      for i = 0 to lt-1 do
+        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
+          Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref
+            i lna vdefj lar
+      done
+
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
@@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
-  let _ = type_fixpoint env1 names lara vdefj in
+  let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
 and execute_array env evdref = Array.map (execute env evdref)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index dafd75231..22cb7f3b9 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -39,3 +39,8 @@ val solve_evars : env -> evar_map ref -> constr -> constr
 (** (first constr is term to match, second is return predicate) *)
 val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
   unit
+
+(** Raise an error message if bodies have types not unifiable with the
+    expected ones *)
+val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
+  Names.Name.t array -> types array -> unsafe_judgment array -> unit
-- 
cgit v1.2.3


From 74f8381ed943f1e786b32c49fb31f14fd488dc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 10 Sep 2016 11:37:21 +0200
Subject: Test for #5077.

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

diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v
new file mode 100644
index 000000000..7e7f2c373
--- /dev/null
+++ b/test-suite/bugs/closed/5077.v
@@ -0,0 +1,8 @@
+(* Testing robustness of typing for a fixpoint with evars in its type *)
+
+Inductive foo (n : nat) : Type := .
+Definition foo_denote {n} (x : foo n) : Type := match x with end.
+
+Definition baz : forall n (x : foo n), foo_denote x.
+refine (fix go n (x : foo n) : foo_denote x := _).
+Abort.  
-- 
cgit v1.2.3


From 469c6be3677c365295fd233319db792385e5c688 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 10 Sep 2016 13:05:50 +0200
Subject: Avoid putting a useless "toploop" directory in the ML search path if
 it does not exist.

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

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 258a1135f..8a8dbe960 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -89,7 +89,8 @@ let init_load_path () =
       Mltop.add_ml_dir (coqlib/"stm");
       Mltop.add_ml_dir (coqlib/"ide")
     end;
-    Mltop.add_ml_dir (coqlib/"toploop");
+    if System.exists_dir (coqlib/"toploop") then
+      Mltop.add_ml_dir (coqlib/"toploop");
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
-- 
cgit v1.2.3


From 650550fc95d5ba41da84e2003371522221e27734 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 18 Jun 2016 19:07:42 -0400
Subject: Add a test for 4836

This required improving the machinery of the test-suite Makefile to
support -compile.
---
 test-suite/Makefile                         | 18 ++++++++++--------
 test-suite/bugs/closed/PLACEHOLDER.v        |  0
 test-suite/bugs/closed/bug_4836.v           |  1 +
 test-suite/bugs/closed/bug_4836/PLACEHOLDER |  0
 4 files changed, 11 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bugs/closed/PLACEHOLDER.v
 create mode 100644 test-suite/bugs/closed/bug_4836.v
 create mode 100644 test-suite/bugs/closed/bug_4836/PLACEHOLDER

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81321729d..c918e92d6 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,6 +49,9 @@ SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
+# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
+has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
+get_command_based_on_flags = $(if $(call has_compile_flag,$(1)),$(coqc),$(command))
 
 
 bogomips:=
@@ -172,7 +175,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
 	@echo "TEST      $<  $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...still active"; \
@@ -193,7 +196,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -256,7 +259,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -311,7 +314,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+	  res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
@@ -341,7 +344,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	      echo $(log_success); \
 	      echo "    $<...still wished"; \
@@ -483,4 +486,3 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
-
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
new file mode 100644
index 000000000..e69de29bb
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
new file mode 100644
index 000000000..5838dcd8a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
new file mode 100644
index 000000000..e69de29bb
-- 
cgit v1.2.3


From 345b6addf7195d39e86827aca9c16f0407aba028 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Wed, 7 Sep 2016 15:43:17 -0700
Subject: Revert the LtacProf tactic table header

This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read.  (This way, the alignment of the headers matches the alignment of the entries.)
---
 ltac/profile_ltac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 3661fe54f..50f9583f9 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -147,7 +147,7 @@ let rec list_iter_is_last f = function
   | x :: xs -> f false x :: list_iter_is_last f xs
 
 let header =
-  str "                                   tactic  local  total   calls       max" ++
+  str " tactic                                   local  total   calls       max " ++
   fnl () ++
   str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++
   fnl ()
-- 
cgit v1.2.3


From 74d2ef26ce991c16039db8c06f813836304c6480 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Sun, 11 Sep 2016 15:49:50 -0700
Subject: Fix newlines in printout of LtacProf

Previously, newlines were missing if a node had no children.
---
 ltac/profile_ltac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 50f9583f9..d2b7c7075 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -160,6 +160,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
     ++ padl 8 (string_of_int e.ncalls)
     ++ padl 10 (format_sec (e.max_total))
   ) ++
+  fnl () ++
   print_table ~filter all_total indent false e.children
 
 and print_table ~filter all_total indent first_level table =
@@ -179,7 +180,7 @@ and print_table ~filter all_total indent first_level table =
      let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
      print_node ~filter all_total (indent ^ sep0) (indent ^ sep1)
     in
-    prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls)
+    prlist (fun pr -> pr) (list_iter_is_last iter ls)
 
 let to_string ~filter node =
   let tree = node.children in
@@ -224,7 +225,6 @@ let to_string ~filter node =
     header ++
     print_table ~filter all_total "" true flat_tree ++
     fnl () ++
-    fnl () ++
     header ++
     print_table ~filter all_total "" true tree
   in
-- 
cgit v1.2.3


From 12cedcbf4dcfe4fd43ab9f4b648314cac26b82db Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 3 Jul 2016 17:13:37 -0400
Subject: Add support for testing output mod timing changes

Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages.  (This can potentially be
extended later.)

Add a test-suite file to make sure that LtacProf outputs some table.
---
 test-suite/Makefile                        | 33 ++++++++++++++++++++++++++++--
 test-suite/output-modulo-time/ltacprof.out | 12 +++++++++++
 test-suite/output-modulo-time/ltacprof.v   |  8 ++++++++
 3 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/output-modulo-time/ltacprof.out
 create mode 100644 test-suite/output-modulo-time/ltacprof.v

diff --git a/test-suite/Makefile b/test-suite/Makefile
index c918e92d6..a3050bfcc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,8 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-get_command_based_on_flags = $(if $(call has_compile_flag,$(1)),$(coqc),$(command))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
 
 
 bogomips:=
@@ -82,7 +83,7 @@ COMPLEXITY := $(if $(bogomips),complexity)
 BUGS := bugs/opened bugs/closed
 
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
-  interactive micromega $(COMPLEXITY) modules stm
+  output-modulo-time interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
@@ -136,6 +137,7 @@ summary:
 	  $(call summary_dir, "Failure tests", failure); \
 	  $(call summary_dir, "Bugs tests", bugs); \
 	  $(call summary_dir, "Output tests", output); \
+	  $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \
 	  $(call summary_dir, "Interactive tests", interactive); \
 	  $(call summary_dir, "Micromega tests", micromega); \
 	  $(call summary_dir, "Miscellaneous tests", misc); \
@@ -291,6 +293,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	  rm $$tmpoutput; \
 	} > "$@"
 
+$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
+	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	    | grep -v "Welcome to Coq" \
+	    | grep -v "\[Loading ML file" \
+	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
+	    | sed 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	    | sed 's/\s*0\.\s*//g' \
+	    > $$tmpoutput; \
+	  sed 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \
+	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (unexpected output)"; \
+	  fi; \
+	  rm $$tmpoutput; \
+	  rm $$tmpexpected; \
+	} > "$@"
+
 $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out
new file mode 100644
index 000000000..cc04c2c9b
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.out
@@ -0,0 +1,12 @@
+total time:      1.528s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
new file mode 100644
index 000000000..d79451f0f
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+  idtac. idtac. sleep. constructor.
+Defined.
-- 
cgit v1.2.3


From 6234ecf5f5752768175d510749cc48a97c2c0dbe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 12 Sep 2016 15:14:23 +0200
Subject: Refolding: disable in 8.4 compat file, document

---
 CHANGES                   |  6 ++++++
 doc/refman/RefMan-tac.tex | 10 ++++++++++
 theories/Compat/Coq84.v   |  3 +++
 3 files changed, 19 insertions(+)

diff --git a/CHANGES b/CHANGES
index 17e397d6e..594bbc831 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,12 @@ Tactics
 
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - Flag "Regular Subst Tactic" is now on by default.
+- New flag "Refolding Reduction", now disabled by default, which turns
+  on refolding of constants/fixpoints (as in cbn) during the reductions
+  done during type inference and tactic retyping. Can be extremely
+  expensive. When set off, this recovers the 8.4 behaviour of unification
+  and type inference. Potential source of incompatibility with 8.5 developments
+  (the option is set on in Compat/Coq85.v).
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
   On by default and deprecated. Minor source of incompatibility
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b668239a6..8172b5771 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3293,6 +3293,16 @@ reduced to \texttt{S t}.
 
 \end{Variants}
 
+\begin{quote}
+\optindex{Refolding Reduction}
+{\tt Refolding Reduction}
+\end{quote}
+
+This option (off by default) controls the use of the refolding strategy
+of {\tt cbn} while doing reductions in unification, type inference and
+tactic applications. It can result in expensive unifications, as
+refolding currently uses a potentially exponential heuristic.
+
 \subsection{\tt unfold \qualid}
 \tacindex{unfold}
 \label{unfold}
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 8ae1a9195..341be92d1 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -25,6 +25,9 @@ Global Set Nonrecursive Elimination Schemes.
 (** See bug 3545 *)
 Global Set Universal Lemma Under Conjunction.
 
+(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *)
+Global Unset Refolding Reduction.
+
 (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
 Ltac constructor_84_n n := constructor n.
 Ltac constructor_84_tac tac := once (constructor; tac).
-- 
cgit v1.2.3


From 90e5945e1666540bc18e7a9b831d136041f4e487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 12 Sep 2016 17:22:03 +0200
Subject: Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.

---
 interp/notation_ops.ml           | 3 ++-
 test-suite/output/Notations2.out | 2 ++
 test-suite/output/Notations2.v   | 5 +++++
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5abc7794b..ec4b2e938 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -577,7 +577,8 @@ let rec alpha_var id1 id2 = function
 
 let add_env alp (sigma,sigmalist,sigmabinders) var v =
   (* Check that no capture of binding variables occur *)
-  if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+  if not (Id.equal ldots_var var) &&
+     List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match;
   (* TODO: handle the case of multiple occs in different scopes *)
   ((var,v)::sigma,sigmalist,sigmabinders)
 
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d3837..13ed7816d 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,5 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7..3f3945052 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
-- 
cgit v1.2.3


From a5fb20b4ad4a56e15455ca329fbc4d03ac5fe072 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 09:35:05 +0200
Subject: feedback: provide a feeder that prints debug messages

---
 lib/feedback.ml  | 5 +++++
 lib/feedback.mli | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 4bda936f2..dd1ca2af3 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -128,6 +128,11 @@ let msg_debug   ?loc x = !logger ?loc Debug x
 let feeders = ref []
 let add_feeder f = feeders := f :: !feeders
 
+let debug_feeder = function
+  | { contents = Message (Debug, loc, pp) } ->
+       msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+  | _ -> ()
+
 let feedback_id    = ref (Edit 0)
 let feedback_route = ref default_route
 
diff --git a/lib/feedback.mli b/lib/feedback.mli
index d19517bb9..48b1c19a6 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -86,6 +86,9 @@ val emacs_logger    : logger
 (** [add_feeder] feeders observe the feedback *)
 val add_feeder : (feedback -> unit) -> unit
 
+(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
+val debug_feeder : feedback -> unit
+
 (** [feedback ?id ?route fb] produces feedback fb, with [route] and
     [id] set appropiatedly, if absent, it will use the defaults set by
     [set_id_for_feedback] *)
-- 
cgit v1.2.3


From 5d3718123afed16691843b5d7bcd5841b18f95ac Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 09:37:08 +0200
Subject: stm: feedback forwarding has to be atomic

I think that a better place for the mutex would be the printing routine,
but I still hope we will get rid of threads in favor of coroutines.
So I keep all mutexes in Stm.
---
 stm/stm.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index cf9fa5492..c53bd958a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -37,10 +37,12 @@ let state_computed, state_computed_hook = Hook.make
 let state_ready, state_ready_hook = Hook.make
  ~default:(fun state_id -> ()) ()
 
-let forward_feedback, forward_feedback_hook = Hook.make
- ~default:(function
+let forward_feedback, forward_feedback_hook = 
+  let m = Mutex.create () in
+  Hook.make ~default:(function
     | { id = id; route; contents } ->
-      feedback ~id:id ~route contents) ()
+        try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+        with e -> Mutex.unlock m; raise e) ()
 
 let parse_error, parse_error_hook = Hook.make
  ~default:(fun id loc msg ->
-- 
cgit v1.2.3


From ef02dca29b1bbeefc15c50e525971b425eeb05b4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 09:39:54 +0200
Subject: coqc: print debug feedback coming from workers

This way par:eauto and all:eato print the same debugging traecs
---
 toplevel/coqtop.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a56459f18..ee331e37c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -227,18 +227,16 @@ let compile_file (v,f) =
     Vernac.compile v f
 
 let compile_files () =
-  match !compile_list with
-    | [] -> ()
-    | [vf] -> compile_file vf (* One compilation : no need to save init state *)
-    | l ->
-      let init_state = States.freeze ~marshallable:`No in
-      let coqdoc_init_state = CLexer.location_table () in
-      List.iter
-        (fun vf ->
-	  States.unfreeze init_state;
-	  CLexer.restore_location_table coqdoc_init_state;
-          compile_file vf)
-        (List.rev l)
+  if !compile_list == [] then ()
+  else
+    let init_state = States.freeze ~marshallable:`No in
+    let coqdoc_init_state = CLexer.location_table () in
+    Feedback.(add_feeder debug_feeder);
+    List.iter (fun vf ->
+        States.unfreeze init_state;
+        CLexer.restore_location_table coqdoc_init_state;
+        compile_file vf)
+      (List.rev !compile_list)
 
 (** Options for proof general *)
 
-- 
cgit v1.2.3


From dd4088ade7539c42adb15f58edcbf7fcf638731c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 09:40:39 +0200
Subject: CoqIDE: push to message win feedback Message(Debug,Info,Notice)

---
 ide/coqOps.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 52f935bf6..1563c7ffb 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -481,6 +481,8 @@ object(self)
           add_flag sentence (`WARNING (loc, msg));
           self#attach_tooltip sentence loc msg;
           self#position_warning_tag_at_sentence sentence loc
+      | Message((Info|Notice|Debug as lvl), _, msg), _ ->
+          messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
-- 
cgit v1.2.3


From 61ad52acc91cc954e39006864f253c0f08b1ba80 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 09:43:46 +0200
Subject: AsyncTaskQueue: annotate debug feedback messages with worker id

---
 stm/asyncTaskQueue.ml | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 49b51b171..fa6422cdc 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -298,10 +298,24 @@ module Make(T : Task) = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
+  let pp_pid pp = 
+    (* Breaking all abstraction barriers... very nice *)
+    let get_xml pp = match Richpp.repr pp with
+      | Xml_datatype.Element("_", [], xml) -> xml
+      | _ -> assert false in
+    Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
+      get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
+      get_xml pp))
+
+  let debug_with_pid = Feedback.(function
+    | { contents = Message(Debug, loc, pp) } as fb ->
+       { fb with contents = Message(Debug,loc,pp_pid pp) }
+    | x -> x)
+
   let main_loop () =
     (* We pass feedback to master *)
     let slave_feeder oc fb =
-      Marshal.to_channel oc (RespFeedback fb) []; flush oc in
+      Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
     Feedback.set_logger Feedback.feedback_logger;
     (* We ask master to allocate universe identifiers *)
-- 
cgit v1.2.3


From 881d38c4c64fb3f3c346d5fbea15999fd6110ae9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 12:55:00 +0200
Subject: test-suite/output-modulo-time made more robust

---
 test-suite/Makefile | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a3050bfcc..1dfbb29ff 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -304,10 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed 's/\s*[0-9]*\.[0-9]\+\s*//g' \
-	    | sed 's/\s*0\.\s*//g' \
+	    | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	          -e 's/\s*0\.\s*//g' \
+		  -e 's/\s*[-+]nan\s*//g' \
+		  -e 's/\s*[-+]inf\s*//g' \
 	    > $$tmpoutput; \
-	  sed 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \
+	  sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+		-e 's/\s*0\.\s*//g' \
+		-e 's/\s*[-+]nan\s*//g' \
+		-e 's/\s*[-+]inf\s*//g' \
+       	       $*.out > $$tmpexpected; \
 	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-- 
cgit v1.2.3


From 93ae6db3375d442ef67154c832bbdf155cffe32f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 13 Sep 2016 13:00:02 +0200
Subject: LtacProp: fix reset_profile (fix #5079)

---
 ltac/profile_ltac.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index d2b7c7075..fe591c775 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -73,7 +73,7 @@ module Local = Summary.Local
 
 let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
 
-let reset_profile () =
+let reset_profile_tmp () =
   Local.(stack := [empty_treenode root]);
   encountered_multi_success_backtracking := false
 
@@ -295,7 +295,7 @@ let exit_tactic start_time c =
   | [] | [_] ->
     (* oops, our stack is invalid *)
     encounter_multi_success_backtracking ();
-    reset_profile ()
+    reset_profile_tmp ()
   | node :: (parent :: rest as full_stack) ->
     let name = string_of_call c in
     if not (String.equal name node.name) then
@@ -330,7 +330,7 @@ let exit_tactic start_time c =
     (* Calls are over, we reset the stack and send back data *)
     if rest == [] && get_profiling () then begin
       assert(String.equal root parent.name);
-      reset_profile ();
+      reset_profile_tmp ();
       feedback_results parent
     end
 
@@ -381,6 +381,10 @@ let _ =
         data := SM.add s (merge_roots results other_results) !data
     | _ -> ()))
 
+let reset_profile () =
+  reset_profile_tmp ();
+  data := SM.empty
+
 (* ******************** *)
 
 let print_results_filter ~filter =
-- 
cgit v1.2.3


From 0e94cb62410354e5df4e65b34e7cbf8451b31d6e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 13 Sep 2016 13:42:04 +0200
Subject: Fixing #5078 (wrong detection of evaluable local hypotheses).

---
 ltac/taccoerce.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index 0110510d3..46469df6a 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -241,9 +241,8 @@ let coerce_to_evaluable_ref env v =
     | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
-    if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
-    else fail ()
+    let ev = EvalVarRef (out_gen (topwit wit_var) v) in
+    if Tacred.is_evaluable env ev then ev else fail ()
   else if has_type v (topwit wit_ref) then
     let open Globnames in
     let r = out_gen (topwit wit_ref) v in
-- 
cgit v1.2.3


From 2aaa58c22e37b05e3637ac7161bb464da7db054a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 14 Sep 2016 10:22:41 +0200
Subject: Fixing test-suite after commit 43104a0b.

---
 test-suite/success/TestRefine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862f..023cb5f59 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3