diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-11 18:59:06 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-11 18:59:06 +0000 |
| commit | 8f72678f7a1fc1d0e2c9ac7a5f682ce100bfa403 (patch) | |
| tree | 4aa74c5721a3b24372cfa0d72784749de204d493 /tactics/tacinterp.ml | |
| parent | 80105c8482bd487782dcab8161fa1fc1f3fdf635 (diff) | |
Use a lazy value for the message in FailError, so that it won't be
unnecessarily computed when the user won't see it (avoids the costly
nf_evar_defs in typeclass errors).
Add hook support for mutual definitions in Program.
Try to solve only the argument typeclasses when calling [refine].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c21a4c080..0942fde83 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1918,7 +1918,7 @@ and eval_with_fail ist is_lazy goal tac = with | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> - raise (Eval_fail s) + raise (Eval_fail (Lazy.force s)) | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) | Stdpp.Exc_located(s,FailError (lvl,s')) -> raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) |