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 /tactics/equality.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 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 0ed754f6f..0144fbb34 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -134,10 +134,10 @@ let general_elim_clause with_evars cls rew elim = an extra condition *) tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false) | Some id -> rewrite_elim_in with_evars id rew elim) - with Pretype_errors.PretypeError (env, - (Pretype_errors.NoOccurrenceFound (c', _))) -> + with Pretype_errors.PretypeError (env,evd, + Pretype_errors.NoOccurrenceFound (c', _)) -> raise (Pretype_errors.PretypeError - (env, (Pretype_errors.NoOccurrenceFound (c', cls)))) + (env,evd,Pretype_errors.NoOccurrenceFound (c', cls))) let general_elim_clause with_evars tac cls sigma c t l l2r elim gl = let all, firstonly, tac = |