From 5ecd8a6a5593d7f197a115b129ebd5f530e40161 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Sep 2016 23:44:44 +0200
Subject: Fix bug #3920 for good after 44ada64.

The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
---
 ltac/rewrite.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index cf59b6dc1f..69f45e1aeb 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1578,11 +1578,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)) <*>
-- 
cgit v1.2.3