From a97decb77b2084a3b84c5135f5bae2dbbb5ace26 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Jun 2010 17:53:35 +0000
Subject: Fixed bug #2135 (second-order unification was raising cryptic
 message) - made the example work (a call to whd_meta was missing) - replaced
 the internal error messages of w_unify_to_subterm_list into  
 user-understandable messages - incidentally fixed the meaning of whd_meta
 (which now takes an evd)   and meta_name (which now does what it means and do
 not treat differently   the instantiated metas)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index bccde6cbd9..e016867506 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -436,6 +436,16 @@ let explain_cannot_find_well_typed_abstraction env p l =
   str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
   str "which is ill-typed."
 
+let explain_abstraction_over_meta _ m n =
+  strbrk "Too complex unification problem: cannot find a solution for both " ++
+  pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+
+let explain_non_linear_unification env m t =
+  strbrk "Cannot unambiguously instantiate " ++
+  pr_name m ++ str ":" ++
+  strbrk " which would require to abstract twice on " ++
+  pr_lconstr_env env t ++ str "."
+
 let explain_type_error env err =
   let env = make_all_name_different env in
   match err with
@@ -489,7 +499,8 @@ let explain_pretype_error env err =
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
   | CannotFindWellTypedAbstraction (p,l) ->
       explain_cannot_find_well_typed_abstraction env p l
-
+  | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
+  | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
 
 (* Typeclass errors *)
 
-- 
cgit v1.2.3