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 /tactics | |
| 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')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
4 files changed, 7 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 0ed754f6f8..0144fbb34c 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 = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0490f1bc89..f9c8e47fd7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -578,7 +578,7 @@ let hResolve id c occ t gl = try Pretyping.Default.understand sigma env t_hole with - | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> + | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 99cbfe4980..860f162dbc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1532,7 +1532,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = with RewriteFailure -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError - (pf_env gl, + (pf_env gl,project gl, Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) let general_s_rewrite_clause x = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d18b540de7..2c4201f99f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -787,9 +787,9 @@ let simplest_elim c = default_elim false (c,NoBindings) let clenv_fchain_in id elim_flags mv elimclause hypclause = try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause - with PretypeError (env,NoOccurrenceFound (op,_)) -> + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) - raise (PretypeError (env,NoOccurrenceFound (op,Some id))) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) let elimination_in_clause_scheme with_evars id i elimclause indclause gl = let indmv = destMeta (nth_arg i elimclause.templval.rebus) in |