diff options
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 16 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
4 files changed, 13 insertions, 11 deletions
diff --git a/dev/include b/dev/include index 99c1a1b6c..15725ae8b 100644 --- a/dev/include +++ b/dev/include @@ -33,6 +33,7 @@ #install_printer (* constr_substituted *) ppsconstr;; #install_printer (* universe *) ppuni;; #install_printer (* universes *) ppuniverses;; +#install_printer (* constraints *) ppconstraints;; #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 34f8f07f9..d2cd0957e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -513,13 +513,6 @@ let mark_resolvability b sigma = let mark_unresolvables sigma = mark_resolvability false sigma let mark_resolvables sigma = mark_resolvability true sigma -let has_typeclasses evd = - Evd.fold_undefined (fun ev evi has -> has || - (is_class_evar evd evi && is_resolvable evi)) - evd false - -let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) - open Evar_kinds type evar_filter = Evar_kinds.t -> bool @@ -529,6 +522,13 @@ let no_goals_or_obligations = function | GoalEvar | QuestionMark _ -> false | _ -> true +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)) + evd false + +let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) + let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd = - if not (has_typeclasses evd) then evd + if not (has_typeclasses filter evd) then evd else !solve_instanciations_problem env evd filter split fail diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 18652b767..b31d3a5fc 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,8 +61,9 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd + in Typeclasses.mark_unresolvables evd' else clenv.evd in let clenv = { clenv with evd = evd' } in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a050e45c3..5aa9c8036 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -775,10 +775,10 @@ let pr_constraints printenv env evm = let explain_unsatisfiable_constraints env evd constr = let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in - (* Remove goal evars *) + (* Remove evars that are not subject to resolution. *) let undef = fold_undefined (fun ev evi evm' -> - if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm + if not (Typeclasses.is_resolvable evi) then Evd.remove evm' ev else evm') evm evm in match constr with | None -> |