Added propagation of evars unification failure reasons for better

error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.

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

4 files changed, 18 insertions, 13 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8c4faa11cf..b5770c8a78 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -431,7 +431,8 @@ 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 (_,_,NotClean _) as e -> raise e
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,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 36268de1ee..3d37074428 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,15 +25,17 @@ let depends_on_evar evk _ (pbty,_,t1,t2) =
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c evd =
-  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 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."
 
 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 2835eb5429..7472918690 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -55,8 +55,9 @@ let rec catchable_exception = function
   | Tacred.ReductionTacticError _ 
   (* unification errors *)
   | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
-		   |CannotFindWellTypedAbstraction _|OccurCheck _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _
+		   |ActualTypeNotCoercible _|UnifOccurCheck _
+		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
   | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 2802acfc1a..87a1e02a86 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -401,7 +401,8 @@ let rec catchable_exception = function
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* unification errors *)
   | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _
+		   |ActualTypeNotCoercible _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
   | Typeclasses_errors.TypeClassError