diff options
| author | msozeau | 2009-06-01 21:19:20 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-01 21:19:20 +0000 |
| commit | ce19a21686b6a75f4fea6f49468812679f241d64 (patch) | |
| tree | ab9b7a74226c084ce2d75d7af4405c34b494e26f | |
| parent | 15d3e64ff69e39b41413831e20b9fe408d3263d5 (diff) | |
## Lines starting with '## ' will be removed from the log message.
## File(s) to commit:
## tactics/refine.ml
Try solving typeclasses before refining in Refine.refine (suggested by
S. Lescuyer).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12157 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |