Permalink
Browse files

Fix for bug #3017: wrong handling of the unresolvability status

in clenvtac and error-printing code. 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16383 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
msozeau
msozeau committed Apr 3, 2013
1 parent f5ab2e3 commit d5b13126177a7f30069d0512f1d08b34e00e3fee
Showing with 13 additions and 11 deletions.
  1. +1 −0 dev/include
  2. +8 −8 pretyping/typeclasses.ml
  3. +2 −1 proofs/clenvtac.ml
  4. +2 −2 toplevel/himsg.ml
View
@@ -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;;
View
@@ -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
View
@@ -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
View
@@ -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 ->

0 comments on commit d5b1312

Please sign in to comment.