diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 21 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 22 | ||||
| -rw-r--r-- | tactics/refine.ml | 2 |
3 files changed, 24 insertions, 21 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 96cef72b44..0486eec58f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -281,13 +281,19 @@ let rec pp_hints_path = function | PathEmpty -> str"Ø" | PathEpsilon -> str"ε" -let rec subst_hints_path subst hp = - match hp with - | PathAtom PathAny -> hp - | PathAtom (PathHints grs) -> +let subst_path_atom subst p = + match p with + | PathAny -> p + | PathHints grs -> let gr' gr = fst (subst_global subst gr) in let grs' = list_smartmap gr' grs in - if grs' == grs then hp else PathAtom (PathHints grs') + if grs' == grs then p else PathHints grs' + +let rec subst_hints_path subst hp = + match hp with + | PathAtom p -> + let p' = subst_path_atom subst p in + if p' == p then hp else PathAtom p' | PathStar p -> let p' = subst_hints_path subst p in if p' == p then hp else PathStar p' | PathSeq (p, q) -> @@ -681,9 +687,10 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let tac' = !forward_subst_tactic subst tac in if tac==tac' then data.code else Extern tac' in + let name' = subst_path_atom subst data.name in let data' = - if data.pat==pat' && data.code==code' then data - else { data with pat = pat'; code = code' } + if data.pat==pat' && data.name == name' && data.code==code' then data + else { data with pat = pat'; name = name'; code = code' } in if k' == k && data' == data then hint else (k',data') in diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4553a8fa51..c8fe1a4267 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -680,25 +680,21 @@ let resolve_all_evars debug m env p oevd do_split fail = docomp evd comps in docomp oevd split -let initial_select_evars with_goals = - if with_goals then - (fun evd ev evi -> - Typeclasses.is_class_evar evd evi) - else - (fun evd ev evi -> - (snd (Evd.evar_source ev evd) <> Evar_kinds.GoalEvar) - && Typeclasses.is_class_evar evd evi) - -let resolve_typeclass_evars debug m env evd with_goals split fail = +let initial_select_evars filter = + fun evd ev evi -> + filter (snd evi.Evd.evar_source) && + Typeclasses.is_class_evar evd evi + +let resolve_typeclass_evars debug m env evd filter 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 with_goals) evd split fail + resolve_all_evars debug m env (initial_select_evars filter) evd 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 solve_inst debug depth env evd filter split fail = + resolve_typeclass_evars debug depth env evd filter split fail let _ = Typeclasses.solve_instanciations_problem := diff --git a/tactics/refine.ml b/tactics/refine.ml index 93c4ea57cf..07480fc000 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 ~with_goals:false (pf_env gl) evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (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 |