diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 6575bbfe1f..3cd02f5444 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1222,9 +1222,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl = with | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> - Refiner.tclFAIL_lazy 0 - (lazy (str"Unable to satisfy the rewriting constraints." - ++ fnl () ++ Himsg.explain_typeclass_error env e)) + Refiner.tclFAIL 0 + (str"Unable to satisfy the rewriting constraints." + ++ fnl () ++ Himsg.explain_typeclass_error env e) in tac gl open Goal |