diff options
author | 2006-11-21 21:38:49 +0000 | |
---|---|---|
committer | 2006-11-21 21:38:49 +0000 | |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /toplevel/himsg.ml | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r-- | toplevel/himsg.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 73aaef30..b8e9eeda 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: himsg.ml 9217 2006-10-05 17:31:23Z notin $ *) open Pp open Util @@ -385,6 +385,14 @@ let explain_cannot_unify m n = str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str"with" ++ brk(1,1) ++ pn +let explain_cannot_unify_local env m n subn = + let pm = pr_lconstr m in + let pn = pr_lconstr n in + let psubn = pr_lconstr_env env subn in + str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str"with" ++ brk(1,1) ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ + psubn ++ str" contains local variables" + let explain_refiner_cannot_generalize ty = str "Cannot find a well-typed generalisation of the goal with type : " ++ pr_lconstr ty @@ -455,6 +463,7 @@ let explain_pretype_error ctx err = | NotProduct c -> explain_not_product ctx c | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotUnifyLocal (e,m,n,sn) -> explain_cannot_unify_local e m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize ty | NoOccurrenceFound c -> explain_no_occurrence_found c | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n |