diff options
| author | herbelin | 2010-11-07 23:35:56 +0000 |
|---|---|---|
| committer | herbelin | 2010-11-07 23:35:56 +0000 |
| commit | d46ed1de8e9c928eed1121ae77bd308ecb88205b (patch) | |
| tree | 9ee1240ccae3c67631997a4299a4e9c80f78473f /proofs | |
| parent | 966a0d7534763c65e65d32b5d6223fd34cfa2445 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.ml | 7 |
3 files changed, 8 insertions, 7 deletions
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 |