diff options
| author | herbelin | 2013-02-17 14:56:11 +0000 |
|---|---|---|
| committer | herbelin | 2013-02-17 14:56:11 +0000 |
| commit | f5e644a53c69392f94eae01dd71ab79b4700a892 (patch) | |
| tree | 592ea17a9580bede8e1aa7dc6dbd878e4e190e63 /toplevel | |
| parent | 358c68e60a4a82dbce209559b94858e917590787 (diff) | |
A more informative message when the elimination predicate for
destruct, rewrite, etc. is not well-typed.
Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 848bf52324..14202a32aa 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -219,7 +219,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let pc,pct = pr_ljudge_env env c in hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in - str "Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ + str "Illegal application: " ++ (* pe ++ *) fnl () ++ str "The term" ++ brk(1,1) ++ pr ++ spc () ++ str "of type" ++ brk(1,1) ++ prt ++ spc () ++ str "cannot be applied to the " ++ term_string1 ++ fnl () ++ @@ -489,12 +489,13 @@ let explain_cannot_unify_binding_type env m n = str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." -let explain_cannot_find_well_typed_abstraction env p l = +let explain_cannot_find_well_typed_abstraction env p l e = str "Abstracting over the " ++ str (String.plural (List.length l) "term") ++ spc () ++ hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++ str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ - str "which is ill-typed." + str "which is ill-typed." ++ + (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e) let explain_wrong_abstraction_type env na abs expected result = let ppname = match na with Anonymous -> mt() | Name id -> pr_id id ++ spc() in @@ -565,8 +566,9 @@ let explain_pretype_error env sigma err = | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n - | CannotFindWellTypedAbstraction (p,l) -> + | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env p l + (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c |