diff options
| author | msozeau | 2012-03-20 18:46:08 +0000 |
|---|---|---|
| committer | msozeau | 2012-03-20 18:46:08 +0000 |
| commit | debb1dba19c079afd7657e8518034209f08bb2b1 (patch) | |
| tree | 65ed66a015b5bab33ac7d51dde167ca37f757928 /tactics | |
| parent | 17ca9766c45ebb368558712eff18d0ed71583e66 (diff) | |
Fix interface of resolve_typeclasses: onlyargs -> with_goals:
by default typeclass resolution is not launched on goal evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 19 | ||||
| -rw-r--r-- | tactics/refine.ml | 2 |
2 files changed, 11 insertions, 10 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 125ef94dcc..24c3a5d9f1 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -677,24 +677,25 @@ let resolve_all_evars debug m env p oevd do_split fail = docomp evd comps in docomp oevd split -let initial_select_evars onlyargs = - if onlyargs then +let initial_select_evars with_goals = + if with_goals then (fun evd ev evi -> - Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) - && Typeclasses.is_class_evar evd evi) + Typeclasses.is_class_evar evd evi) else - (fun evd ev evi -> Typeclasses.is_class_evar evd evi) + (fun evd ev evi -> + (snd (Evd.evar_source ev evd) <> Evd.GoalEvar) + && Typeclasses.is_class_evar evd evi) -let resolve_typeclass_evars debug m env evd onlyargs split fail = +let resolve_typeclass_evars debug m env evd with_goals split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd with _ -> evd in - resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail + resolve_all_evars debug m env (initial_select_evars with_goals) evd split fail -let solve_inst debug depth env evd onlyargs split fail = - resolve_typeclass_evars debug depth env evd onlyargs split fail +let solve_inst debug depth env evd with_goals split fail = + resolve_typeclass_evars debug depth env evd with_goals split fail let _ = Typeclasses.solve_instanciations_problem := diff --git a/tactics/refine.ml b/tactics/refine.ml index fa023e78e9..93c4ea57cf 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -389,7 +389,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = let refine (evd,c) gl = let sigma = project gl in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in + let evd = Typeclasses.resolve_typeclasses ~with_goals:false (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 |