diff options
| -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 9d9847ea57..08055004fd 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1477,7 +1477,7 @@ let assert_replacing id newt tac = else decl :: nc') env ~init:[] in - Proofview.Refine.refine begin fun sigma -> + Proofview.Refine.refine ~unsafe:false begin fun sigma -> let env' = Environ.reset_with_named_context (val_of_named_context nc') env in let sigma, ev = Evarutil.new_evar env' sigma concl in let sigma, ev' = Evarutil.new_evar env sigma newt in @@ -1507,7 +1507,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match is_hyp, prf with | Some id, Some p -> - let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1521,7 +1521,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let (sigma, ev) = Evarutil.new_evar env sigma newt in sigma, mkApp (p, [| ev |]) in - Proofview.Refine.refine make <*> Proofview.Unsafe.tclNEWGOALS gls + Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> |