diff options
| -rw-r--r-- | tactics/refine.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 1a61c982b5..46c8d3aa2e 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -369,10 +369,12 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = (* Et finalement la tactique refine elle-même : *) -let refine oc gl = +let refine (evd,c) gl = let sigma = project gl in - let (sigma,c) = Evarutil.evars_to_metas sigma oc in + let evd = Typeclasses.resolve_typeclasses (pf_env gl) evd in + let c = Evarutil.nf_evar evd c in + let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise complicated to update meta types when passing through a binder *) - let th = compute_metamap (pf_env gl) sigma c in - tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl + let th = compute_metamap (pf_env gl) evd c in + tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl |