From 4d5d2abcbaff682cbc07a68e8bab91008f4bfe98 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 22 Jun 2017 10:58:54 +0200 Subject: [PATCH] fix(init/meta): fix build --- library/init/meta/smt/interactive.lean | 2 +- library/init/meta/tactic.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index b6535d4bc8..64cee71ee4 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -22,7 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit := tac >> solve_goals meta def istep {α : Type} (line0 col0 line col : nat) (tac : smt_tactic α) : smt_tactic unit := -λ ss ts, (@scope_trace _ line col ((tac >> solve_goals) ss ts)).clamp_pos line0 line col +λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals) ss ts)).clamp_pos line0 line col meta def execute (tac : smt_tactic unit) : tactic unit := using_smt tac diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 629975c894..fd77a70238 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -477,7 +477,7 @@ meta def step {α : Type u} (t : tactic α) : tactic unit := t >>[tactic] cleanup meta def istep {α : Type u} (line0 col0 : ℕ) (line col : ℕ) (t : tactic α) : tactic unit := -λ s, (@scope_trace _ line col (step t s)).clamp_pos line0 line col +λ s, (@scope_trace _ line col (λ _, step t s)).clamp_pos line0 line col meta def is_prop (e : expr) : tactic bool := do t ← infer_type e,