diff options
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 |