Quelques bricoles autour de l'unification:

- Un patch pour le bug de non vérification du typage de Stéphane L.
- Changement du fameux message "cannot solve a second-order matching problem"
  en espérant, à défaut de savoir résoudre plus souvent le problème, que
  le message est plus explicite.
- Divers changements cosmétiques.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10860 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 2 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4950f4064d..70450295be 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -403,7 +403,7 @@ let explain_cannot_unify_local env m n subn =
       psubn ++ str " contains local variables"
 
 let explain_refiner_cannot_generalize env ty =
-  str "Cannot find a well-typed generalisation of the goal with type : " ++
+  str "Cannot find a well-typed generalisation of the goal with type: " ++
   pr_lconstr_env env ty
 
 let explain_no_occurrence_found env c id =
@@ -419,6 +419,16 @@ 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
 
+let explain_cannot_find_well_typed_abstraction env p l =
+  let la,lc = list_chop (List.length l - 1) l in
+  str "Abstracting over the " ++
+  str (plural (List.length l) "term") ++ spc () ++ 
+  hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++
+         (if la<>[] then str " and" ++ spc () else mt()) ++ 
+         pr_lconstr_env env (List.hd lc)) ++ spc () ++
+  str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ 
+  str "which is ill-typed"
+
 let explain_type_error env err =
   let env = make_all_name_different env in
   match err with
@@ -470,6 +480,8 @@ let explain_pretype_error env 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) ->
+      explain_cannot_find_well_typed_abstraction env p l
 
       
 (* Typeclass errors *)
@@ -716,7 +728,7 @@ let explain_cannot_infer_predicate env typs =
   let env = make_all_name_different env in
   let pr_branch (cstr,typ) =
     let cstr,_ = decompose_app cstr in
-    str "For " ++ pr_lconstr_env env cstr ++ str " : " ++ pr_lconstr_env env typ
+    str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ
   in
   str "Unable to unify the types found in the branches:" ++
   spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))