From a9122a2c0ae7b3632b58b2dfc307cb629e16ef47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Feb 2017 19:51:40 -0800 Subject: [PATCH] chore(library/init/meta): use general when --- library/init/meta/smt/rsimp.lean | 2 +- library/init/meta/tactic.lean | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean index 6f7f67824a..baffb8ee1d 100644 --- a/library/init/meta/smt/rsimp.lean +++ b/library/init/meta/smt/rsimp.lean @@ -103,7 +103,7 @@ do t ← target, try (replace_target new_t pr) meta def rsimplify_at (ccs : cc_state) (h : expr) (m : option repr_map := none) : tactic unit := -do tactic.when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"), +do when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"), htype ← infer_type h, (new_htype, heq) ← rsimplify ccs htype m, try $ do assert (expr.local_pp_name h) new_htype, diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 44b51fff7c..8ded8ff5df 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -716,10 +716,6 @@ do g::gs ← get_goals, meta instance : has_andthen (tactic unit) := ⟨seq⟩ -/- Applies tac if c holds -/ -meta def when (c : Prop) [decidable c] (tac : tactic unit) : tactic unit := -if c then tac else skip - meta constant is_trace_enabled_for : name → bool /- Execute tac only if option trace.n is set to true. -/