From d46ed1de8e9c928eed1121ae77bd308ecb88205b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 7 Nov 2010 23:35:56 +0000
Subject: 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
---
 proofs/clenv.ml     | 2 +-
 proofs/logic.ml     | 6 +++---
 proofs/proofview.ml | 7 ++++---
 3 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 70f2f6b64a..71d952caf9 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -448,7 +448,7 @@ 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 (_,_,NotClean _) as e -> raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 593ef0b329..5b55e1c02f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -48,13 +48,13 @@ open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
   | LtacLocated(_,e) -> catchable_exception e
-  | Util.UserError _ | TypeError _
+  | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
   | RefinerError _ | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* reduction errors *)
   | Tacred.ReductionTacticError _ 
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _|OccurCheck _
 		   |UnsolvableImplicit _)) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 677c739428..2802acfc1a 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -395,11 +395,12 @@ let rec tclGOALBINDU s k =
 open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
-  | Util.UserError _ | Type_errors.TypeError _ 
+  | Util.UserError _
+  | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
   | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
-- 
cgit v1.2.3