From 6cbd65aa4e5fe82259b44b89e5e624ed2299249c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Mar 2011 20:11:32 +0000
Subject: 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
---
 pretyping/pretype_errors.mli | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 30ee6aaf67..f95514ade4 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -17,15 +17,26 @@ 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
-  (** Unification *)
-  | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * Evd.hole_kind
+  (** Type inference unification *)
+  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+  (** Tactic Unification *)
+  | UnifOccurCheck of existential_key * constr
   | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
       Evd.unsolvability_explanation option
-  | CannotUnify of constr * constr
+  | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
@@ -59,7 +70,8 @@ val jv_nf_betaiotaevar :
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+      unification_error -> 'b
 
 val error_cant_apply_not_functional_loc :
   loc -> env -> Evd.evar_map ->
@@ -93,14 +105,12 @@ 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 -> constr * constr -> 'b
+val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
+  constr * constr -> 'b
 
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
-- 
cgit v1.2.3