diff options
| author | Pierre-Marie Pédrot | 2016-09-08 23:44:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-09 00:08:21 +0200 |
| commit | 5ecd8a6a5593d7f197a115b129ebd5f530e40161 (patch) | |
| tree | d2023cfab1224ebb6f8f8ffb2edf44eb5deb6802 | |
| parent | e65c629bac48e61b3a14f05bfafc6b85486359c0 (diff) | |
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.
| -rw-r--r-- | ltac/rewrite.ml | 3 |
1 files changed, 1 insertions, 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)) <*> |