diff options
| author | msozeau | 2008-01-18 19:41:43 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-18 19:41:43 +0000 |
| commit | c2e3d63ca60b27abb5398ecbc8ebcaf8fb925206 (patch) | |
| tree | f0a1603b98484520e841283140817bc783d86a37 /toplevel | |
| parent | f57b2e6cf26316ec7df340ab95399039dae5143e (diff) | |
Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a wrapper around Ltac program_simpl ::= .
!!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 23 |
1 files changed, 20 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 784346b244..0b69c41e79 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -343,8 +343,25 @@ let explain_not_clean env ev t k = str "with a term using variable " ++ var ++ spc () ++ str "which is not in its scope." -let explain_unsolvable_implicit env k = - str "Cannot infer " ++ explain_hole_kind env k ++ str "." +let pr_ne_context_of header footer env = + if Environ.rel_context env = empty_rel_context & + Environ.named_context env = empty_named_context then footer + else pr_ne_context_of header env + +let explain_typeclass_resolution env evi k = + match k with + InternalHole | ImplicitArg _ -> + (match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + str"." ++ 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 -> str ".") + | _ -> str "." + +let explain_unsolvable_implicit env evi k = + str "Cannot infer " ++ explain_hole_kind env k ++ explain_typeclass_resolution env evi k let explain_var_not_found env id = str "The variable" ++ spc () ++ pr_id id ++ @@ -432,7 +449,7 @@ let explain_pretype_error env err = | CantFindCaseType c -> explain_cant_find_case_type env c | OccurCheck (n,c) -> explain_occur_check env n c | NotClean (n,c,k) -> explain_not_clean env n c k - | UnsolvableImplicit k -> explain_unsolvable_implicit env k + | UnsolvableImplicit (evi,k) -> explain_unsolvable_implicit env evi k | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect | NotProduct c -> explain_not_product env c |