Merge branch 'v8.6'

3 files changed, 13 insertions, 11 deletions

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 3661fe54f2..fe591c7756 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 8e74249de9..a332e28716 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 0110510d35..46469df6a1 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