Reverted commit r13893 about propagation of more informative

unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).

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

18 files changed, 144 insertions, 258 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 27dcffcea..f1f5d4c9f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -120,7 +120,6 @@ let pr_global_env = pr_global_env
 let pr_global = pr_global_env Idset.empty
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
-let pr_existential_key evk = str (string_of_existential evk)
 let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
 let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
 let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 6a256bd59..ca91cfd4f 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -76,7 +76,6 @@ val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
 val pr_global              : global_reference -> std_ppcmds
 
 val pr_constant            : env -> constant -> std_ppcmds
-val pr_existential_key     : existential_key -> std_ppcmds
 val pr_existential         : env -> existential -> std_ppcmds
 val pr_constructor         : env -> constructor -> std_ppcmds
 val pr_inductive           : env -> inductive -> std_ppcmds
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 5e574ce53..4f8344745 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1576,7 +1576,7 @@ let constr_of_pat env isevars arsign pat avoid =
 		    in
 		    let neq = eq_id avoid id in
 		      (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
-		  with NotUnifiable _ -> sign, 1, avoid
+		  with Reduction.NotConvertible -> sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
 		  pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 2610ed4ed..5a2d84057 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -112,7 +112,7 @@ module Coercion = struct
 	try
 	  isevars := the_conv_x_leq env x y !isevars;
 	  None
-	with NotUnifiable _ -> coerce' env x y
+	with Reduction.NotConvertible -> coerce' env x y
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
       let dest_prod c =
@@ -129,12 +129,12 @@ module Coercion = struct
 		let (n, eqT), restT = dest_prod typ in
 		let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
-	      with NotUnifiable _ ->
+	      with Reduction.NotConvertible ->
 		let (n, eqT), restT = dest_prod typ in
 		let (n', eqT'), restT' = dest_prod typ' in
 		let _ =
 		  try isevars := the_conv_x_leq env eqT eqT' !isevars
-		  with NotUnifiable _ -> raise NoSubtacCoercion
+		  with Reduction.NotConvertible -> raise NoSubtacCoercion
 		in
 		(* Disallow equalities on arities *)
 		if Reduction.is_arity env eqT then raise NoSubtacCoercion;
@@ -323,7 +323,6 @@ module Coercion = struct
 
   (* appliquer le chemin de coercions de patterns p *)
   exception NoCoercion
-  exception NoCoercionNoUnifier of evar_map * unification_error
 
   let apply_pattern_coercion loc pat p =
     List.fold_left
@@ -419,12 +418,12 @@ module Coercion = struct
       with Not_found -> raise NoCoercion
     in
       try (the_conv_x_leq env t' c1 evd, v')
-      with NotUnifiable _ -> raise NoCoercion
+      with Reduction.NotConvertible -> raise NoCoercion
 
 
   let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try (the_conv_x_leq env t c1 evd, v)
-    with NotUnifiable (best_failed_evd,e) ->
+    with Reduction.NotConvertible ->
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
@@ -448,7 +447,7 @@ module Coercion = struct
         let t2 = Termops.subst_term v1 t2 in
 	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
 	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
-    | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
+    | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
@@ -459,12 +458,12 @@ module Coercion = struct
 	      inh_conv_coerce_to_fail loc env evd rigidonly
 		(Some (nf_evar evd cj.uj_val))
 		(nf_evar evd cj.uj_type) (nf_evar evd t)
-	    with NoCoercionNoUnifier (best_failed_evd,e) ->
+	    with NoCoercion ->
 	      let sigma =  evd in
 		try
 		  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 		with NoSubtacCoercion ->
-		  error_actual_type_loc loc env sigma cj t e
+		  error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
 	    (evd',{ uj_val = val'; uj_type = t })
@@ -491,7 +490,7 @@ module Coercion = struct
 	  in
 	    try
 	      fst (try inh_conv_coerce_to_fail loc env' isevars false None t t'
-		   with NoCoercionNoUnifier _ ->
+		   with NoCoercion ->
 		     coerce_itf loc env' isevars None t t')
 	    with NoSubtacCoercion ->
 	      error_cannot_coerce env' isevars (t, t'))
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bedd3eb74..5503a147a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,7 +79,6 @@ end
 module Default = struct
   (* Typing operations dealing with coercions *)
   exception NoCoercion
-  exception NoCoercionNoUnifier of evar_map * unification_error
 
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
@@ -187,11 +186,11 @@ module Default = struct
       with Not_found -> raise NoCoercion
     in
       try (the_conv_x_leq env t' c1 evd, v')
-      with NotUnifiable _ -> raise NoCoercion
+      with Reduction.NotConvertible -> raise NoCoercion
 
   let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try (the_conv_x_leq env t c1 evd, v)
-    with NotUnifiable (best_failed_evd,e) ->
+    with Reduction.NotConvertible ->
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
@@ -219,7 +218,7 @@ module Default = struct
 	  | Some v2 -> Retyping.get_type_of env1 evd' v2 in
 	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
 	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
-    | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
+    | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
@@ -228,12 +227,12 @@ module Default = struct
 	  let (evd', val') =
 	    try
 	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-	    with NoCoercionNoUnifier (best_failed_evd,e) ->
+	    with NoCoercion ->
 	      let evd = saturate_evd env evd in
 		try
 		  inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-		with NoCoercionNoUnifier _ ->
-		  error_actual_type_loc loc env best_failed_evd cj t e
+		with NoCoercion ->
+		  error_actual_type_loc loc env evd cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
 	    (evd',{ uj_val = val'; uj_type = t })
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 183cb1c95..3906f8728 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,7 +19,6 @@ open Recordops
 open Evarutil
 open Libnames
 open Evd
-open Pretype_errors
 
 type flex_kind_of_term =
   | Rigid of constr
@@ -129,42 +128,39 @@ let rec ise_try evd = function
     [] -> assert false
   | [f] -> f evd
   | f1::l ->
-      match f1 evd with
-      | Success _ as x -> x
-      | UnifFailure _ -> ise_try evd l
+      let (evd',b) = f1 evd in
+      if b then (evd',b) else ise_try evd l
 
 let ise_and evd l =
   let rec ise_and i = function
       [] -> assert false
     | [f] -> f i
     | f1::l ->
-        match f1 i with
-	| Success i' -> ise_and i' l
-	| UnifFailure _ as x -> x in
+        let (i',b) = f1 i in
+        if b then  ise_and i' l else (evd,false) in
   ise_and evd l
 
 let ise_list2 evd f l1 l2 =
   let rec ise_list2 i l1 l2 =
     match l1,l2 with
-        [], [] -> Success i
+        [], [] -> (i, true)
       | [x], [y] -> f i x y
       | x::l1, y::l2 ->
-          (match f i x y with
-	  | Success i' -> ise_list2 i' l1 l2
-	  | UnifFailure _ as x -> x)
-      | _ -> UnifFailure (evd, NotSameArgSize) in
+          let (i',b) = f i x y in
+          if b then ise_list2 i' l1 l2 else (evd,false)
+      | _ -> (evd, false) in
   ise_list2 evd l1 l2
 
 let ise_array2 evd f v1 v2 =
   let rec allrec i = function
-    | -1 -> Success i
+    | -1 -> (i,true)
     | n ->
-        match f i v1.(n) v2.(n) with
-	| Success i' -> allrec i' (n-1)
-	| UnifFailure _ as x -> x in
+        let (i',b) = f i v1.(n) v2.(n) in
+        if b then allrec i' (n-1) else (evd,false)
+  in
   let lv1 = Array.length v1 in
   if lv1 = Array.length v2 then allrec evd (pred lv1)
-  else UnifFailure (evd,NotSameArgSize)
+  else (evd,false)
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -180,8 +176,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
       else None
     else None in
   match ground_test with
-    | Some true -> Success evd
-    | Some false -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+      Some b -> (evd,b)
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
@@ -222,12 +217,9 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and i
             [(fun i -> ise_list2 i
                   (fun i -> evar_conv_x ts env i CONV) l1 l2);
-             (fun i ->
-	       Success (solve_refl
-                  (fun env i pbty a1 a2 ->
-		    is_success (evar_conv_x ts env i pbty a1 a2))
-	          env i sp1 al1 al2))]
-          else UnifFailure (i,NotSameHead)
+             (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2,
+                  true)]
+          else (i,false)
 	in
 	ise_try evd [f1; f2]
 
@@ -255,12 +247,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               [(fun i -> ise_list2 i
                   (fun i -> evar_conv_x ts env i CONV) l1 rest2);
                (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
-          else UnifFailure (i,NotSameArgSize)
+          else (i,false)
 	and f2 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
-	    | None -> UnifFailure (i,NotSameHead)
+	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
 
@@ -287,12 +279,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               [(fun i -> ise_list2 i
                   (fun i -> evar_conv_x ts env i CONV) rest1 l2);
                (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
-          else UnifFailure (i,NotSameArgSize)
+          else (i,false)
 	and f2 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
-	    | None -> UnifFailure (i,NotSameHead)
+	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
 
@@ -319,12 +311,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  if flex1 = flex2 then
 	    ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2
 	  else
-	     UnifFailure (i,NotSameHead)
+	     (i,false)
 	and f2 i =
 	  (try conv_record ts env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
-           with Not_found -> UnifFailure (i,NoCanonicalStructure))
+           with Not_found -> (i,false))
 	and f3 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
@@ -339,7 +331,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		match eval_flexible_term env flex2 with
 		| Some v2 ->
 		    evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
-		| None -> UnifFailure (i,NotSameHead)
+		| None -> (i,false)
 	  else
 	    match eval_flexible_term env flex2 with
 	    | Some v2 ->
@@ -348,7 +340,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		match eval_flexible_term env flex1 with
 		| Some v1 ->
 		    evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
-		| None -> UnifFailure (i,NotSameHead)
+		| None -> (i,false)
 	in
 	ise_try evd [f1; f2; f3]
       end
@@ -395,7 +387,8 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (position_problem true pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd)
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
+	  true
 
     | (Rigid _ | PseudoRigid _), Flexible ev2 ->
 	if
@@ -410,29 +403,30 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (position_problem false pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd)
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
+	  true
 
     | MaybeFlexible flex1, (Rigid _ | PseudoRigid _) ->
 	let f3 i =
 	  (try conv_record ts env i (check_conv_record appr1 appr2)
-           with Not_found -> UnifFailure (i,NoCanonicalStructure))
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
  		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
-	    | None -> UnifFailure (i,NotSameHead)
+	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
     | (Rigid _ | PseudoRigid _), MaybeFlexible flex2 ->
 	let f3 i =
 	  (try conv_record ts env i (check_conv_record appr2 appr1)
-           with Not_found -> UnifFailure (i,NoCanonicalStructure))
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
  		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
-	    | None -> UnifFailure (i,NotSameHead)
+	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
@@ -440,8 +434,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
         match kind_of_term c1, kind_of_term c2 with
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            if base_sort_cmp pbty s1 s2 then Success evd
-	    else UnifFailure (evd,NotSameHead)
+	    (evd, base_sort_cmp pbty s1 s2)
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
@@ -453,12 +446,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| Ind sp1, Ind sp2 ->
 	    if eq_ind sp1 sp2 then
               ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
-            else UnifFailure (evd,NotSameHead)
+            else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
 	    if eq_constructor sp1 sp2 then
               ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
-            else UnifFailure (evd,NotSameHead)
+            else (evd, false)
 
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
             if i1=i2  then
@@ -470,12 +463,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x ts env i CONV) l1 l2)]
-            else UnifFailure (evd,NotSameHead)
+            else (evd,false)
 
-	| (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ ->
-	    UnifFailure (evd,NotSameHead)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) ->
-	    UnifFailure (evd,NotSameHead)
+	| (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> (evd,false)
+	| _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> (evd,false)
 
 	| (App _ | Meta _ | Cast _ | Case _ | Fix _), _ -> assert false
 	| (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
@@ -504,10 +495,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
 	         (fun i -> ise_list2 i
                      (fun i -> evar_conv_x ts env i CONV) l1 l2)]
-	    else UnifFailure (evd,NotSameHead)
+	    else (evd,false)
 
 	| (Meta _ | Case _ | Fix _ | CoFix _),
-	  (Meta _ | Case _ | Fix _ | CoFix _) -> UnifFailure (evd,NotSameHead)
+	  (Meta _ | Case _ | Fix _ | CoFix _) -> (evd,false)
 
 	| (App _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> assert false
 	| _, (App _ | Ind _ | Construct _ | Sort _ | Prod _) -> assert false
@@ -520,9 +511,9 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
       end
 
-    | PseudoRigid _, Rigid _ -> UnifFailure (evd,NotSameHead)
+    | PseudoRigid _, Rigid _ ->  (evd,false)
 
-    | Rigid _, PseudoRigid _ -> UnifFailure (evd,NotSameHead)
+    | Rigid _, PseudoRigid _ ->  (evd,false)
 
 and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let (evd',ks,_) =
@@ -578,12 +569,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       & array_for_all (fun a -> a = term2 or isEvar a) args1 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
-      Success (choose_less_dependent_instance evk1 evd term2 args1)
+      choose_less_dependent_instance evk1 evd term2 args1, true
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
       & array_for_all (fun a -> a = term1 or isEvar a) args2 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
-      Success (choose_less_dependent_instance evk2 evd term1 args2)
+      choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       first_order_unification ts env evd (ev1,l1) appr2
@@ -598,10 +589,8 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = List.fold_left
     (fun evd (pbty,env,t1,t2) ->
-      match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
-      | Success evd' -> evd'
-      | UnifFailure (evd,reason) ->
-	  Pretype_errors.error_cannot_unify env evd ~reason (t1, t2))
+      let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
+	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
     evd pbs in
     Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
 			  |_,ImpossibleCase -> 
@@ -610,24 +599,22 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
 
 (* Main entry points *)
 
-exception NotUnifiable of evar_map * unification_error
-
 let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd =
   match evar_conv_x ts env evd CONV  t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e))
+      (evd',true) -> evd'
+    | _ -> raise Reduction.NotConvertible
 
 let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
   match evar_conv_x ts env evd CUMUL t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e))
+      (evd', true) -> evd'
+    | _ -> raise Reduction.NotConvertible
 
 let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
   match evar_conv_x ts env !evd CONV t1 t2 with
-  | Success evd' -> evd := evd'; true
-  | _ -> false
+      (evd',true) -> evd := evd'; true
+    | _ -> false
 
 let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
   match evar_conv_x ts env !evd CUMUL t1 t2 with
-  | Success evd' -> evd := evd'; true
-  | _ -> false
+      (evd',true) -> evd := evd'; true
+    | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index d2d74ff96..e1f507b0a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -13,9 +13,7 @@ open Environ
 open Reductionops
 open Evd
 
-exception NotUnifiable of evar_map * Pretype_errors.unification_error
-
-(** returns exception NotUnifiable with best known evar_map if not unifiable *)
+(** returns exception Reduction.NotConvertible if not unifiable *)
 val the_conv_x     : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
 val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
 
@@ -27,11 +25,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -
 (**/**)
 (* For debugging *)
 val evar_conv_x : transparent_state ->
-  env -> evar_map -> conv_pb -> constr -> constr -> Evarutil.unification_result
+  env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
 val evar_eqappr_x : transparent_state ->
   env -> evar_map ->
     conv_pb -> constr * constr list -> constr * constr list ->
-      Evarutil.unification_result
+      evar_map * bool
 (**/**)
 
 val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 13d193658..774180c67 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -584,9 +584,6 @@ let clear_hyps_in_evi evdref hyps concl ids =
   in
   (nhyps,nconcl)
 
-(***************)
-(* Unification *)
-
 (* Inverting constructors in instances (common when inferring type of match) *)
 
 let find_projectable_constructor env evd cstr k args cstr_subst =
@@ -948,7 +945,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
   (* Filter and restrict if needed *)
   let evd,evk,args =
     restrict_upon_filter evd evi evk
-      (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2)
+      (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
       (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
   (* Leave a unification problem *)
   let args1,args2 = List.split args in
@@ -979,17 +976,9 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
  *                Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
  *)
 
-type unification_result =
-  | Success of evar_map
-  | UnifFailure of evar_map * unification_error
-
-let is_success = function Success _ -> true | UnifFailure _ -> false
-
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
 exception OccurCheckIn of evar_map * constr
-exception MetaOccurInBodyInternal
-exception InstanceNotSameTypeInternal
 
 let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let aliases = make_alias_map env in
@@ -1104,7 +1093,7 @@ and occur_existential evm c =
 and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd =
   try
     let (evd',body) = invert_definition choose env evd ev rhs in
-    if occur_meta body then raise MetaOccurInBodyInternal;
+    if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar evk body then raise (OccurCheckIn (evd',body));
@@ -1130,17 +1119,18 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd =
   with
     | NotEnoughInformationToProgress ->
 	postpone_evar_term env evd ev rhs
-    | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
-        raise e
+    | NotInvertibleUsingOurAlgorithm t ->
+	error_not_clean env evd evk t (evar_source evk evd)
     | OccurCheckIn (evd,rhs) ->
 	(* last chance: rhs actually reduces to ev *)
 	let c = whd_betadeltaiota env evd rhs in
 	match kind_of_term c with
 	| Evar (evk',argsv2) when evk = evk' ->
-	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
+	    solve_refl
+	      (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
 	      env evd evk argsv argsv2
 	| _ ->
-	    raise (OccurCheckIn (evd,rhs))
+	    error_occur_check env evd evk rhs
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
@@ -1317,10 +1307,10 @@ let check_instance_type conv_algo env evd ev1 t2 =
     if isEvar typ2 then (* Don't want to commit too early too *) evd
     else
       let typ1 = existential_type evd ev1 in
-      match conv_algo env evd Reduction.CUMUL typ2 typ1 with
-      | Success evd -> evd
-      | UnifFailure _ ->
-	  raise InstanceNotSameTypeInternal
+      let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
+      if b then evd else
+	user_err_loc (fst (evar_source (fst ev1) evd),"",
+	  str "Unable to find a well-typed instantiation")
 
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
@@ -1334,9 +1324,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
 	  if evk1 = evk2 then
-	    solve_refl
-	      (fun env evd pbty a b -> is_success (conv_algo env evd pbty a b))
-	      env evd evk1 args1 args2
+	    solve_refl conv_algo env evd evk1 args1 args2
 	  else
 	    if pbty = None
 	    then solve_evar_evar evar_define env evd ev1 ev2
@@ -1365,20 +1353,11 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
     in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
       List.fold_left
-	(fun p (pbty,env,t1,t2) ->
-	  match p with
-	  | Success evd -> conv_algo env evd pbty t1 t2
-	  | UnifFailure _ as x -> x) (Success evd)
+	(fun (evd,b as p) (pbty,env,t1,t2) ->
+	  if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
 	pbs
-  with
-    | NotInvertibleUsingOurAlgorithm t ->
-        UnifFailure (evd,NotClean (evk1,t))
-    | OccurCheckIn (evd,rhs) ->
-        UnifFailure (evd,OccurCheck (evk1,rhs))
-    | MetaOccurInBodyInternal ->
-        UnifFailure (evd,MetaOccurInBody evk1)
-    | InstanceNotSameTypeInternal ->
-        UnifFailure (evd,InstanceNotSameType evk1)
+  with e when precatchable_exception e ->
+    (evd,false)
 
 (** The following functions return the set of evars immediately
     contained in the object, including defined evars *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 705ab356f..a4c07a019 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -74,20 +74,13 @@ val whd_head_evar :  evar_map -> constr -> constr
 val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 val solve_refl :
-  (env ->  evar_map -> conv_pb -> constr -> constr -> bool)
+  (env ->  evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
   -> env ->  evar_map -> existential_key -> constr array -> constr array ->
     evar_map
-
-type unification_result =
-  | Success of evar_map
-  | UnifFailure of evar_map * Pretype_errors.unification_error
-
-val is_success : unification_result -> bool
-
 val solve_simple_eqn :
-  (env ->  evar_map -> conv_pb -> constr -> constr -> unification_result)
+  (env ->  evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
   -> ?choose:bool -> env ->  evar_map -> bool option * existential * constr ->
-    unification_result
+    evar_map * bool
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f663496df..6d1c54e63 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,26 +18,15 @@ open Type_errors
 open Glob_term
 open Inductiveops
 
-type unification_error =
-  | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr
-  | NotSameArgSize
-  | NotSameHead
-  | NoCanonicalStructure
-  | ConversionFailed of env * constr * constr
-  | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key
-
 type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
-  (* Type inference unification *)
-  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
-  (* Tactic unification *)
-  | UnifOccurCheck of existential_key * constr
+  (* Unification *)
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr * Evd.hole_kind
   | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
       Evd.unsolvability_explanation option
-  | CannotUnify of constr * constr * unification_error option
+  | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
@@ -106,15 +95,6 @@ let contract2 env a b = match contract env [a;b] with
 let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
-let contract4 env a b c d = match contract env [a;b;c;d] with
-  | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
-
-let contract3' env a b c = function
-  | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
-  | NotClean (evk,d) -> let x,d = contract4 env a b c d in x,NotClean(evk,d)
-  | NotSameArgSize | NotSameHead | NoCanonicalStructure  | ConversionFailed _
-  | MetaOccurInBody _ | InstanceNotSameType _ as x -> contract3 env a b c, x
-
 let raise_pretype_error (loc,env,sigma,te) =
   Loc.raise loc (PretypeError(env,sigma,te))
 
@@ -122,11 +102,10 @@ let raise_located_type_error (loc,env,sigma,te) =
   Loc.raise loc (PretypeError(env,sigma,TypingError te))
 
 
-let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason =
-  let (env, c, actty, expty), reason = contract3' env c actty expty reason in
+let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
+  let env, c, actty, expty = contract3 env c actty expty in
   let j = {uj_val=c;uj_type=actty} in
-  raise_pretype_error
-    (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason))
+  raise_located_type_error (loc, env, sigma, ActualType (j, expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
   raise_located_type_error
@@ -158,20 +137,23 @@ let error_not_a_type_loc loc env sigma j =
     a precise location. *)
 
 let error_occur_check env sigma ev c =
-  raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
+  raise (PretypeError (env, sigma, OccurCheck (ev,c)))
+
+let error_not_clean env sigma ev c (loc,k) =
+  Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
   Loc.raise loc
     (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
-let error_cannot_unify env sigma ?reason (m,n) =
-  raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
+let error_cannot_unify env sigma (m,n) =
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
   raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
 
 let error_cannot_coerce env sigma (m,n) =
-  raise (PretypeError (env, sigma,CannotUnify (m,n,None)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_find_well_typed_abstraction env sigma p l =
   raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index f95514ade..30ee6aaf6 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -17,26 +17,15 @@ open Inductiveops
 
 (** {6 The type of errors raised by the pretyper } *)
 
-type unification_error =
-  | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr
-  | NotSameArgSize
-  | NotSameHead
-  | NoCanonicalStructure
-  | ConversionFailed of env * constr * constr
-  | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key
-
 type pretype_error =
   (** Old Case *)
   | CantFindCaseType of constr
-  (** Type inference unification *)
-  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
-  (** Tactic Unification *)
-  | UnifOccurCheck of existential_key * constr
+  (** Unification *)
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr * Evd.hole_kind
   | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
       Evd.unsolvability_explanation option
-  | CannotUnify of constr * constr * unification_error option
+  | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
@@ -70,8 +59,7 @@ val jv_nf_betaiotaevar :
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
-      unification_error -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
   loc -> env -> Evd.evar_map ->
@@ -105,12 +93,14 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
+val error_not_clean :
+  env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
+
 val error_unsolvable_implicit :
   loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind ->
       Evd.unsolvability_explanation option -> 'b
 
-val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
-  constr * constr -> 'b
+val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
 
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 003f507dc..1ea2dbd00 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -640,8 +640,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			try 
 			  ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
 			with Reduction.NotConvertible -> 
-			  error_actual_type_loc loc env !evdref cj tval
-			    (ConversionFailed (env,cty,tval))
+			  error_actual_type_loc loc env !evdref cj tval 
 		      end
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6e39d9831..6121ba7d8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -638,11 +638,9 @@ let order_metas metas =
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
 let solve_simple_evar_eqn ts env evd ev rhs =
-  match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
-  | UnifFailure (evd,reason) ->
-      error_cannot_unify env evd ~reason (mkEvar ev,rhs);
-  | Success evd ->
-      Evarconv.consider_remaining_unif_problems env evd
+  let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in
+  if not b then error_cannot_unify env evd (mkEvar ev,rhs);
+  Evarconv.consider_remaining_unif_problems env evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b5770c8a7..8c4faa11c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -431,8 +431,7 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e ->
-	  raise e
+      | PretypeError (_,_,NotClean _) as e -> raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3d3707442..36268de1e 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,17 +25,15 @@ let depends_on_evar evk _ (pbty,_,t1,t2) =
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c evd =
-  let evd = define evk c evd in
-  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
-  match
-    List.fold_left
-      (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
-	| UnifFailure _ as x -> x) (Success evd)
-      pbs
-  with
-    | Success evd -> evd
-    | UnifFailure _ -> error "Instance does not satisfy the constraints."
+  try
+    let evd = define evk c evd in
+    let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+    fst (List.fold_left
+      (fun (evd,b as p) (pbty,env,t1,t2) ->
+	if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true)
+      pbs)
+  with e when Pretype_errors.precatchable_exception e ->
+    error "Instance does not satisfy constraints."
 
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 747291869..2835eb542 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -55,9 +55,8 @@ let rec catchable_exception = function
   | Tacred.ReductionTacticError _ 
   (* unification errors *)
   | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _
-		   |ActualTypeNotCoercible _|UnifOccurCheck _
-		   |CannotFindWellTypedAbstraction _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+		   |CannotFindWellTypedAbstraction _|OccurCheck _
 		   |UnsolvableImplicit _)) -> true
   | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 87a1e02a8..2802acfc1 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -401,8 +401,7 @@ let rec catchable_exception = function
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* unification errors *)
   | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _
-		   |ActualTypeNotCoercible _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
   | Typeclasses_errors.TypeClassError 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f86d6d271..6af1f9d56 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -153,46 +153,16 @@ let explain_generalization env (name,var) j =
   str "it has type" ++ spc () ++ pt ++
   spc () ++ str "which should be Set, Prop or Type."
 
-let explain_unification_error env p1 p2 = function
-  | None -> mt()
-  | Some e ->
-    match e with
-    | OccurCheck (evk,rhs) ->
-        spc () ++ str "(cannot define " ++ quote (pr_existential_key evk) ++
-	strbrk " with term " ++ pr_lconstr_env env rhs ++
-        strbrk "that would depend on itself)"
-    | NotClean (evk,c) ->
-        spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk)
-        ++ strbrk " because " ++ pr_lconstr_env env c ++
-	strbrk " is out of scope)"
-    | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
-        (* Error speaks from itself *) mt ()
-    | ConversionFailed (env,t1,t2) ->
-        if t1 <> p1 || t2 <> p2 then
-          spc () ++ str "(cannot unify " ++ pr_lconstr_env env t1 ++
-	  strbrk " and " ++ pr_lconstr_env env t2 ++ str ")"
-	else mt ()
-    | MetaOccurInBody evk ->
-        spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++
-	strbrk " refers to a metavariable - please report your example)"
-    | InstanceNotSameType evk ->
-        spc () ++ str "(unable to find a well-typed instantiation for " ++
-	quote (pr_existential_key evk) ++ str ")"
-
-
-let explain_actual_type env sigma j t reason =
+let explain_actual_type env sigma j pt =
   let j = j_nf_betaiotaevar sigma j in
-  let t = Reductionops.nf_betaiota sigma t in
+  let pt = Reductionops.nf_betaiota sigma pt in
   let pe = pr_ne_context_of (str "In environment") env in
   let (pc,pct) = pr_ljudge_env env j in
-  let pt = pr_lconstr_env env t in
-  let ppreason = explain_unification_error env j.uj_type t reason in
+  let pt = pr_lconstr_env env pt in
   pe ++
-  hov 0 (
   str "The term" ++ brk(1,1) ++ pc ++ spc () ++
-  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
-  str "while it is expected to have type" ++ brk(1,1) ++ pt ++
-  ppreason ++ str ".")
+  str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
+  str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "."
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let randl = jv_nf_betaiotaevar sigma randl in
@@ -450,14 +420,13 @@ let explain_wrong_case_info env ind ci =
     str "was given to a pattern-matching expression on the inductive type" ++
     spc () ++ pc ++ str "."
 
-let explain_cannot_unify env sigma m n e =
+let explain_cannot_unify env sigma m n =
   let m = nf_evar sigma m in
   let n = nf_evar sigma n in
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
-  let ppreason = explain_unification_error env m n e in
   str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
-  str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."
+  str "with" ++ brk(1,1) ++ pn ++ str "."
 
 let explain_cannot_unify_local env sigma m n subn =
   let pm = pr_lconstr_env env m in
@@ -525,7 +494,7 @@ let explain_type_error env sigma err =
   | Generalization (nvar, c) ->
       explain_generalization env nvar c
   | ActualType (j, pt) ->
-      explain_actual_type env sigma j pt None
+      explain_actual_type env sigma j pt
   | CantApplyBadType (t, rator, randl) ->
       explain_cant_apply_bad_type env sigma t rator randl
   | CantApplyNonFunctional (rator, randl) ->
@@ -542,13 +511,13 @@ let explain_pretype_error env sigma err =
   let env = make_all_name_different env in
   match err with
   | CantFindCaseType c -> explain_cant_find_case_type env sigma c
-  | ActualTypeNotCoercible (j,t,e) -> explain_actual_type env sigma j t (Some e)
-  | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
+  | OccurCheck (n,c) -> explain_occur_check env sigma n c
+  | NotClean (n,c,k) -> explain_not_clean env sigma n c k
   | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp
   | VarNotFound id -> explain_var_not_found env id
   | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect
   | NotProduct c -> explain_not_product env sigma c
-  | CannotUnify (m,n,e) -> explain_cannot_unify env sigma m n e
+  | CannotUnify (m,n) -> explain_cannot_unify env sigma m n
   | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
   | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id