diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c14f107ec..6da662422 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -481,19 +481,19 @@ let mark_unresolvable evi = mark_resolvability false evi let mark_resolvable evi = mark_resolvability true evi open Evar_kinds -type evar_filter = Evar_kinds.t -> bool +type evar_filter = existential_key -> Evar_kinds.t -> bool -let all_evars _ = true -let all_goals = function GoalEvar -> true | _ -> false -let no_goals evi = not (all_goals evi) -let no_goals_or_obligations = function +let all_evars _ _ = true +let all_goals _ = function GoalEvar -> true | _ -> false +let no_goals ev evi = not (all_goals ev evi) +let no_goals_or_obligations _ = function | GoalEvar | QuestionMark _ -> false | _ -> true let mark_resolvability filter b sigma = Evd.fold_undefined (fun ev evi evs -> - if filter (snd evi.evar_source) then + if filter ev (snd evi.evar_source) then Evd.add evs ev (mark_resolvability_undef b evi) else Evd.add evs ev evi) sigma (Evd.defined_evars sigma) @@ -503,7 +503,7 @@ let mark_resolvables sigma = mark_resolvability all_evars true sigma let has_typeclasses filter evd = Evd.fold_undefined (fun ev evi has -> has || - (filter (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi)) + (filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi)) evd false let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) |