Merge branch 'v8.6'

52 files changed, 397 insertions, 172 deletions

diff --git a/.gitignore b/.gitignore
index d91a674e1..9653564d4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,6 +55,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
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-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.
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/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
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index af87aae1b..6b29b6d3d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -615,7 +615,8 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
      notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then
      we keep (z,x) in alp, and we have to check that what the [v] which is bound
      to [var] does not contain z *)
-  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;
   (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
      with an actual term "fun z => ... z ..." when "x" is bound in the
      notation and the name "x" cannot be changed to "z", e.g. because
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ef4b50130..7d76ecf3a 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) ->
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] *)
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 3661fe54f..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
 
@@ -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 ()
@@ -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
@@ -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 =
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 8e74249de..a332e2871 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1581,11 +1581,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)) <*>
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
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db8cbf231..a063cbbfe 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")
@@ -2094,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/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/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cd7ce89e0..b7fc2de95 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -316,7 +316,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
@@ -434,7 +434,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
@@ -451,7 +452,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/pretyping.ml b/pretyping/pretyping.ml
index 385e100e2..13e5ea97a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -349,21 +349,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.ExtraEnv.env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body ~loc env.ExtraEnv.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
@@ -653,7 +638,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { 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.ExtraEnv.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/reductionops.ml b/pretyping/reductionops.ml
index 7ee70d9e0..494d27178 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/typeclasses.ml b/pretyping/typeclasses.ml
index 4c33a9c78..4207eccb9 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 }
@@ -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/pretyping/typing.ml b/pretyping/typing.ml
index 696d419af..e79e3d46f 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 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 e524edcca..04e5e40bc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -39,3 +39,8 @@ val e_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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8feb34e3e..594732a5a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -480,8 +480,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
 
@@ -573,7 +573,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/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
 
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
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 41ad7d94e..34443b93d 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/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 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 482bbe4c2..3964e6b5c 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 ->
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index 75dd38fde..b8c07512f 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81321729d..1dfbb29ff 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,6 +49,10 @@ 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)))
+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:=
@@ -79,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
@@ -133,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); \
@@ -172,7 +177,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 +198,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 +231,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 +261,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 +276,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" \
@@ -288,6 +293,39 @@ $(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 -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 -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); \
+	    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){ \
@@ -311,7 +349,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 +379,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 +521,3 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
-
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/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.  
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/bugs/closed/PLACEHOLDER.v
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
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
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.
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.
+
+
 
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.
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/Notations2.out b/test-suite/output/Notations2.out
index 20101f48e..5541ccf57 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -58,3 +58,5 @@ exist (Q x) y conj
      : nat -> nat
 % j
      : nat -> nat
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 3cf89818d..1d8278c08 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -111,3 +111,8 @@ Check (exist (Q x) y conj).
 Notation "% i" := (fun i : nat => i) (at level 0, i ident).
 Check %i.
 Check %j.
+
+(* 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}).
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/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.
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.
 
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).
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
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 59ee95b31..7ff59c471 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 []
@@ -90,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 *)
@@ -108,7 +108,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/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 *)
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index f9e0bc34a..6b62f7aeb 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 = {
@@ -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 6e632999c..eebc9ff66 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)