diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-07 23:35:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-07 23:35:56 +0000 |
| commit | d46ed1de8e9c928eed1121ae77bd308ecb88205b (patch) | |
| tree | 9ee1240ccae3c67631997a4299a4e9c80f78473f /proofs/logic.ml | |
| 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/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 593ef0b32..5b55e1c02 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 |