diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d2cd0957e8..25109ffcf0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -505,23 +505,27 @@ let mark_resolvability b evi = let mark_unresolvable evi = mark_resolvability false evi let mark_resolvable evi = mark_resolvability true evi -let mark_resolvability b sigma = - Evd.fold_undefined (fun ev evi evs -> - Evd.add evs ev (mark_resolvability_undef b evi)) - sigma (Evd.defined_evars sigma) - -let mark_unresolvables sigma = mark_resolvability false sigma -let mark_resolvables sigma = mark_resolvability true sigma - open Evar_kinds type evar_filter = Evar_kinds.t -> bool let all_evars _ = true -let no_goals = function GoalEvar -> false | _ -> true +let all_goals = function GoalEvar -> true | _ -> false +let no_goals evi = not (all_goals 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 + Evd.add evs ev (mark_resolvability_undef b evi) + else Evd.add evs ev evi) + sigma (Evd.defined_evars sigma) + +let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma +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)) |