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.

2 files changed, 19 insertions, 9 deletions

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))
diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v
new file mode 100644
index 0000000000..a4adb23cc2
--- /dev/null
+++ b/test-suite/bugs/closed/3920.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+Axiom P : nat -> Prop.
+Axiom P_or : forall x y, P (x + y) <-> P x \/ P y.
+Lemma foo (H : P 3) : False.
+eapply or_introl in H.
+erewrite <- P_or in H.
+(* Error: No such hypothesis: H *)