Permalink
Browse files

Fix typeclass error handling which was sometimes raising a Failure ("…

…hd").

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15593 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent c8178de commit f13b87b5b1a2f5d35b1be51d25d0891a2db08b95 msozeau committed Jul 11, 2012
Showing with 17 additions and 16 deletions.
  1. +3 −3 tactics/rewrite.ml4
  2. +14 −13 toplevel/himsg.ml
View
@@ -1222,9 +1222,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
with
| Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
- Refiner.tclFAIL_lazy 0
- (lazy (str"Unable to satisfy the rewriting constraints."
- ++ fnl () ++ Himsg.explain_typeclass_error env e))
+ Refiner.tclFAIL 0
+ (str"Unable to satisfy the rewriting constraints."
+ ++ fnl () ++ Himsg.explain_typeclass_error env e)
in tac gl
open Goal
View
@@ -395,7 +395,7 @@ let explain_typeclass_resolution env evi k =
fnl () ++ str "Could not find an instance for " ++
pr_lconstr_env env evi.evar_concl ++
pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
- | None -> mt()
+ | _ -> mt()
let explain_unsolvable_implicit env evi k explain =
str "Cannot infer " ++ explain_evar_kind env (Some evi) k ++
@@ -696,12 +696,8 @@ let explain_no_instance env (_,id) l =
let is_goal_evar evi = match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false
let pr_constraints printenv env evm =
- let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in
- let evm = fold_undefined
- (fun ev evi evm' ->
- if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
- in
let l = Evd.to_list evm in
+ assert(l <> []);
let (ev, evi) = List.hd l in
if List.for_all (fun (ev', evi') ->
eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
@@ -717,18 +713,23 @@ let pr_constraints printenv env evm =
pr_evar_map None evm
let explain_unsatisfiable_constraints env evd constr =
- let evm = Evarutil.nf_evar_map evd in
- let undef = Evd.undefined_evars evm in
+ let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in
+ (* Remove goal evars *)
+ let undef = fold_undefined
+ (fun ev evi evm' ->
+ if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
+ in
match constr with
| None ->
str"Unable to satisfy the following constraints:" ++ fnl() ++
pr_constraints true env undef
| Some (ev, k) ->
- explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
- if List.length (Evd.to_list undef) > 1 then
- str"With the following constraints:" ++ fnl() ++
- pr_constraints false env (Evd.remove undef ev)
- else mt ()
+ explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++
+ (let remaining = Evd.remove undef ev in
+ if Evd.has_undefined remaining then
+ str"With the following constraints:" ++ fnl() ++
+ pr_constraints false env remaining
+ else mt ())
let explain_mismatched_contexts env c i j =
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++

0 comments on commit f13b87b

Please sign in to comment.