diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 92d0ac983d..06fea367af 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -345,11 +345,18 @@ END (**********************************************************************) (* Refine *) +let constr_flags = { + Pretyping.use_typeclasses = true; + Pretyping.use_unif_heuristics = true; + Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } + let refine_tac simple {Glob_term.closure=closure;term=term} = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let flags = Pretyping.all_no_fail_flags in + let flags = constr_flags in let tycon = Pretyping.OfType concl in let lvar = { Pretyping.empty_lvar with Pretyping.ltac_constrs = closure.Glob_term.typed; |