aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml2
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')))