diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /toplevel/himsg.ml | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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 |