amelioration des messages d'erreurs vis a vis des evars

ajout automatique des chemins vers les sources au moment du Drop


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

1 files changed, 43 insertions, 18 deletions

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 717191aa8..90d90120e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -14,8 +14,8 @@ open Names
 open Term
 open Sign
 open Environ
-open Type_errors
 open Rawterm
+open Inductive
 (*i*)
 
 (*s The type of errors raised by the pretyper *)
@@ -26,7 +26,7 @@ type ml_case_error =
 
 type pretype_error =
   (* Old Case *)
-  | MlCase of ml_case_error
+  | MlCase of ml_case_error * inductive_type * unsafe_judgment
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of int * constr
@@ -38,42 +38,67 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-val error_cant_find_case_type_loc :
-  loc -> env -> constr -> 'a
+(* Presenting terms without solved evars *)
+val nf_evar : 'a Evd.evar_map -> constr -> constr
+val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar :
+  'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val error_ill_formed_branch_loc : 
-  loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
+(* Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> constr -> constr -> constr -> 'b
+  loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc : 
-  loc -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+  loc -> env -> 'a Evd.evar_map ->
+      unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc : 
-  loc -> env -> int * constr * constr -> 
+  loc -> env -> 'a Evd.evar_map -> int * constr * constr -> 
       unsafe_judgment -> unsafe_judgment list -> 'b
 
-val error_number_branches_loc : 
-  loc -> path_kind -> env -> constr -> constr -> int -> 'b
+val error_cant_find_case_type_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> path_kind -> env -> constr -> constr -> 'b
+  loc -> path_kind -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b
+
+val error_ill_formed_branch_loc : 
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      constr -> int -> constr -> constr -> 'b
+
+val error_number_branches_loc : 
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      unsafe_judgment -> int -> 'b
+
+val error_ill_typed_rec_body_loc :
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      int -> name array -> unsafe_judgment array -> types array -> 'b
 
 (*s Implicit arguments synthesis errors *)
 
-val error_occur_check : env -> int -> constr -> 'a
+val error_occur_check : env -> 'a Evd.evar_map -> int -> constr -> 'b
 
-val error_not_clean : env -> int -> constr -> 'a
+val error_not_clean : env -> 'a Evd.evar_map -> int -> constr -> 'b
 
 (*s Ml Case errors *)
 
-val error_ml_case_loc : loc -> env -> ml_case_error -> 'a
+val error_ml_case_loc :
+  loc -> env -> 'a Evd.evar_map ->
+      ml_case_error -> inductive_type -> unsafe_judgment -> 'b
 
 (*s Pretyping errors *)
 
-val error_var_not_found_loc : loc -> identifier -> 'a
+val error_unexpected_type_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> constr -> 'b
+
+val error_not_product_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> 'b
 
-val error_unexpected_type_loc : loc -> env -> constr -> constr -> 'b
+(*s Error in conversion from AST to rawterms *)
 
-val error_not_product_loc : loc -> env -> constr -> 'a
+val error_var_not_found_loc : loc -> identifier -> 'b