From 2d0ddf7e75b16d73b41db4d4bf0bd1243569e03c Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 19 Mar 2019 19:46:15 -0400 Subject: [PATCH] feat(tactic/wlog): `discharger` defaults to classical `tauto` --- src/tactic/wlog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/wlog.lean b/src/tactic/wlog.lean index cd224ab0ad2a3..cefb82122b4ab 100644 --- a/src/tactic/wlog.lean +++ b/src/tactic/wlog.lean @@ -156,7 +156,7 @@ meta def wlog (cases : parse (tk ":=" *> texpr)?) (perms : parse (tk "using" *> (list_of (ident*) <|> (λx, [x]) <$> ident*))?) (discharger : tactic unit := - (tactic.solve_by_elim <|> tactic.tautology <|> using_smt (smt_tactic.intros >> smt_tactic.solve_goals))) : + (tactic.solve_by_elim <|> tactic.tautology tt <|> using_smt (smt_tactic.intros >> smt_tactic.solve_goals))) : tactic unit := do perms ← parse_permutations perms, (pat, cases_pr, cases_goal, vars, perms) ← (match cases with