diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index dee720fc5..2aa0534a5 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -4,7 +4,7 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic algebra.binary -open tactic binary eq.ops eq +open binary eq.ops eq open decidable namespace experiment definition refl := @eq.refl @@ -27,7 +27,7 @@ definition to_nat [coercion] (n : num) : ℕ := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics - definition apply_refl := apply @refl + definition apply_refl := tactic.apply @refl tactic_hint apply_refl end helper_tactics open helper_tactics diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 1ea1782e6..af66f4c9c 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -4,7 +4,7 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic algebra.binary -open tactic binary eq.ops eq +open binary eq.ops eq open decidable namespace experiment @@ -23,7 +23,7 @@ definition to_nat [coercion] (n : num) : ℕ := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics - definition apply_refl := apply @eq.refl + definition apply_refl := tactic.apply @eq.refl tactic_hint apply_refl end helper_tactics open helper_tactics