diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 67d21886b..4c06550d4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1539,7 +1539,7 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Proofview.Refine.refine ~unsafe:false { run = begin fun sigma -> + Refine.refine ~unsafe:false { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map d = @@ -1568,7 +1568,7 @@ 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 = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in Sigma (mkApp (p, [| ev |]), sigma, q) end } in - Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls + Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls end } | None, None -> Proofview.Unsafe.tclEVARS undef <*> |