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 --- tactics/equality.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/equality.ml') 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 = -- cgit v1.2.3