From 09bf8921fe3744da65965ebca31a3ca409957560 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Sep 2016 14:55:10 -0700 Subject: [PATCH] chore(library/init/meta/interactive): improve error message --- library/init/meta/interactive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 887da4e0e8..6d258a74ba 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -163,7 +163,7 @@ do e ← to_expr p, tactic.generalize e x meta def trivial : tactic unit := -tactic.triv <|> tactic.reflexivity <|> tactic.contradiction +tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed" meta def contradiction : tactic unit := tactic.contradiction