diff options
Diffstat (limited to 'ltac')
| -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 cf59b6dc1..69f45e1ae 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)) <*> |