From 801c1c288e1a82a6eeacf7518b2a2a53f4d09c75 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 2 Dec 2014 18:29:30 +0100
Subject: For compatibility purpose, when setoid_rewriting a hypothesis,
 beta-iota normalize it afterwards.

---
 tactics/rewrite.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6523903bd4..1245e7c298 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1529,6 +1529,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
   in
   let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
   let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in
+  let opt_beta = match clause with
+  | None -> Proofview.tclUNIT ()
+  | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp))
+  in
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1545,7 +1549,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma (res, is_hyp) <*>
       (** For compatibility *)
-      beta <*> Proofview.shelve_unifiable
+      beta <*> opt_beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
       raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
-- 
cgit v1.2.3