From cc6d4a6ef8f465df3bc8d34e8554163c9e9fed3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Dec 2016 09:04:27 -0800 Subject: [PATCH] chore(library/init/meta/interactive): typo --- library/init/meta/interactive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ff32fdb1d7..7f1dfd7896 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -391,7 +391,7 @@ tactic.symmetry meta def transitivity : tactic unit := tactic.transitivity -meta def ac_reflixivity : tactic unit := +meta def ac_reflexivity : tactic unit := tactic.ac_refl meta def ac_refl : tactic unit :=