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

1 files changed, 12 insertions, 1 deletions

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 *)