Delayed the evar normalization in error messages to the last minute

before the message is delivered to the user. Should avoid useless
computation in heavily backtracking tactics (auto, try, ...).

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

1 files changed, 21 insertions, 20 deletions

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d81adb6b0..cdf6b523c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -37,47 +37,48 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of Type_errors.type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 val precatchable_exception : exn -> bool
 
 (** Presenting terms without solved evars *)
-val nf_evar :  Evd.evar_map -> constr -> constr
-val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
-   Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+val nf_evar : Evd.evar_map -> constr -> constr
+val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
+val env_nf_evar : Evd.evar_map -> env -> env
+val jv_nf_betaiotaevar :
+  Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env ->  Evd.evar_map -> int * constr * constr ->
+  loc -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
@@ -87,7 +88,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 (** {6 Implicit arguments synthesis errors } *)
 
-val error_occur_check : env ->  Evd.evar_map -> existential_key -> 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
@@ -112,15 +113,15 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to rawterms } *)