diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 698f46559..b71e51314 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -373,7 +373,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in - Proofview.Refine.refine_casted (fun h -> Proofview.Refine.update h update) <*> + Proofview.Refine.refine ~unsafe:false (fun h -> Proofview.Refine.update h update) <*> Proofview.V82.tactic (reduce refine_red_flags refine_locs) end |