From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 18:47:45 +0200
Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

---
 tactics/class_tactics.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6e01a676a2..8d6c085e63 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1500,9 +1500,11 @@ let head_of_constr h c =
   let c = head_of_constr c in
   letin_tac None (Name h) c None Locusops.allHyps
 
-let not_evar c = match kind_of_term c with
-| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
-| _ -> Proofview.tclUNIT ()
+let not_evar c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match Evarutil.kind_of_term_upto sigma c with
+  | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+  | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
   if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
-- 
cgit v1.2.3


From 18046e2525300b990db4c8817f1cc02dcab97445 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Sep 2016 09:59:20 +0200
Subject: Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal
 calls are logged too. Using appropriate printer for reparsability of the
 output.

---
 tactics/tactics.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index acc0fa1ca7..c9cec828c1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -869,14 +869,17 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
+  let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+  Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter { enter = begin fun gl ->
-  let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
-  let redexps = reduction_clause redexp cl in
+  let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+  let redexps = reduction_clause redexp cl' in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
   end }
+  end
 
 (* Unfolding occurrences of a constant *)
 
-- 
cgit v1.2.3


From c9c54122d1d9493a965b483939e119d52121d5a6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Sep 2016 10:03:18 +0200
Subject: Fixing call to "lazy beta iota" in "refine" (restoring v8.4
 behavior).

(It was reducing also in hypotheses.)
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 54977dbce7..a66dbd6e88 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4589,7 +4589,7 @@ module New = struct
   let reduce_after_refine =
     Proofview.V82.tactic (reduce
       (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences })
+      {onhyps=Some []; concl_occs=AllOccurrences })
 
   let refine ?unsafe c =
     Proofview.Refine.refine ?unsafe c <*>
-- 
cgit v1.2.3