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

2 files changed, 10 insertions, 11 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 5e574ce538..4f8344745e 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 2610ed4ed7..5a2d840570 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'))