From dfbcb72f387679f8bed65bc84cb4d94cebbcc8cb Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 18 Jul 2017 21:28:09 +0100 Subject: [PATCH] chore(init/meta/tactic): remove superfluous fail clause --- library/init/meta/tactic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 50a3a9af8a..f7a6849070 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -1005,8 +1005,7 @@ meta def by_cases (e : expr) (h : name) : tactic unit := do dec_e ← (mk_app `decidable [e] <|> fail "by_cases tactic failed, type is not a proposition"), inst ← (mk_instance dec_e <|> fail "by_cases tactic failed, type of given expression is not decidable"), t ← target, - tm ← (mk_mapp `dite [some e, some inst, some t] <|> - fail "by_cases tactic failed, type of given expression is not decidable"), + tm ← mk_mapp `dite [some e, some inst, some t], seq (apply tm) (intro h >> skip) private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i :=