From e2de6ab28b87f8a26c3f6fc2e9ab57e17f8ecbd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Oct 2016 19:51:12 -0700 Subject: [PATCH] fix(library/init/meta/simp_tactic): typo --- library/init/meta/simp_tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 6b4cd6d735..dbf3d1a695 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -115,7 +115,7 @@ do t ← to_expr `(caching_user_attribute simp_lemmas), v ← to_expr `(({ name := %%a, descr := "simplifier attribute", mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns}, - dependencies := [`reducible] } : caching_user_attribute simp_lemmas)), + dependencies := [`reducibility] } : caching_user_attribute simp_lemmas)), add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff), attribute.register attr_name