From 44ada644ef50563aa52cfcd7717d44bde29e5a20 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 17:37:27 +0200
Subject: Fix bug #3920: eapply masks an hypothesis name.

The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
---
 ltac/rewrite.ml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

(limited to 'ltac')

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 7acad20d20..8cc50684e2 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1561,6 +1561,10 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
+  (** For compatibility *)
+  let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
+  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
+  let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
@@ -1572,12 +1576,17 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+            let tac = Tacticals.New.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
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (id, newt))
+            convert_hyp_no_check (LocalAssum (id, newt)) <*>
+            beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter { enter = begin fun gl ->
@@ -1592,12 +1601,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
-  let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
-  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
-  let opt_beta = match clause with
-  | None -> Proofview.tclUNIT ()
-  | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp)
-  in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1622,7 +1625,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res <*>
       (** For compatibility *)
-      beta <*> opt_beta <*> Proofview.shelve_unifiable
+      beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
       raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
-- 
cgit v1.2.3


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.

---
 ltac/extratactics.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index be47293fcd..e50b0520bc 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -816,9 +816,11 @@ END
 
 TACTIC EXTEND is_evar
 | [ "is_evar" constr(x) ] ->
-    [ match kind_of_term x with
+    [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+      match Evarutil.kind_of_term_upto sigma x with
         | Evar _ -> Proofview.tclUNIT ()
         | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
+      end
     ]
 END
 
-- 
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.

---
 ltac/tacinterp.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 397cd988da..83d67c8e32 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1822,13 +1822,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
         Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma)
       end }
-      end
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-- 
cgit v1.2.3