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 35efb0b65..ca65f08ec 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -357,7 +357,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 env evd lvar tycon term in - Tactics.New.refine ~unsafe:false update + Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable end TACTIC EXTEND refine |