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

1 files changed, 9 insertions, 11 deletions

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