diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index bdf9cce866..a1f1c3157e 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -117,7 +117,7 @@ definition change (e : expr) : tactic := builtin
 
 definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-definition notetac (id : identifier) (e : expr) : tactic := builtin
+definition note_tac (id : identifier) (e : expr) : tactic := builtin
 
 definition constructor (k : option num)  : tactic := builtin
 definition fconstructor (k : option num) : tactic := builtin
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 531c55a9ac..136dd337ae 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -121,7 +121,7 @@ definition change (e : expr) : tactic := builtin
 
 definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-definition notetac (id : identifier) (e : expr) : tactic := builtin
+definition note_tac (id : identifier) (e : expr) : tactic := builtin
 
 definition constructor (k : option num)  : tactic := builtin
 definition fconstructor (k : option num) : tactic := builtin
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index be8f19b872..307fe913bb 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -230,7 +230,7 @@ name const * g_tactic_interleave = nullptr;
 name const * g_tactic_intro = nullptr;
 name const * g_tactic_intros = nullptr;
 name const * g_tactic_none_expr = nullptr;
-name const * g_tactic_notetac = nullptr;
+name const * g_tactic_note_tac = nullptr;
 name const * g_tactic_now = nullptr;
 name const * g_tactic_opt_expr = nullptr;
 name const * g_tactic_opt_expr_list = nullptr;
@@ -488,7 +488,7 @@ void initialize_constants() {
     g_tactic_intro = new name{"tactic", "intro"};
     g_tactic_intros = new name{"tactic", "intros"};
     g_tactic_none_expr = new name{"tactic", "none_expr"};
-    g_tactic_notetac = new name{"tactic", "notetac"};
+    g_tactic_note_tac = new name{"tactic", "note_tac"};
     g_tactic_now = new name{"tactic", "now"};
     g_tactic_opt_expr = new name{"tactic", "opt_expr"};
     g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"};
@@ -747,7 +747,7 @@ void finalize_constants() {
     delete g_tactic_intro;
     delete g_tactic_intros;
     delete g_tactic_none_expr;
-    delete g_tactic_notetac;
+    delete g_tactic_note_tac;
     delete g_tactic_now;
     delete g_tactic_opt_expr;
     delete g_tactic_opt_expr_list;
@@ -1005,7 +1005,7 @@ name const & get_tactic_interleave_name() { return *g_tactic_interleave; }
 name const & get_tactic_intro_name() { return *g_tactic_intro; }
 name const & get_tactic_intros_name() { return *g_tactic_intros; }
 name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; }
-name const & get_tactic_notetac_name() { return *g_tactic_notetac; }
+name const & get_tactic_note_tac_name() { return *g_tactic_note_tac; }
 name const & get_tactic_now_name() { return *g_tactic_now; }
 name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; }
 name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 4f69fe1749..968e2a6594 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -232,7 +232,7 @@ name const & get_tactic_interleave_name();
 name const & get_tactic_intro_name();
 name const & get_tactic_intros_name();
 name const & get_tactic_none_expr_name();
-name const & get_tactic_notetac_name();
+name const & get_tactic_note_tac_name();
 name const & get_tactic_now_name();
 name const & get_tactic_opt_expr_name();
 name const & get_tactic_opt_expr_list_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 5097a8e526..de3eaac762 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -225,7 +225,7 @@ tactic.interleave
 tactic.intro
 tactic.intros
 tactic.none_expr
-tactic.notetac
+tactic.note_tac
 tactic.now
 tactic.opt_expr
 tactic.opt_expr_list
diff --git a/src/library/tactic/note_tactic.cpp b/src/library/tactic/note_tactic.cpp
index 1bee540904..550426a073 100644
--- a/src/library/tactic/note_tactic.cpp
+++ b/src/library/tactic/note_tactic.cpp
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr mk_note_tactic_expr(name const &id, expr const &e) {
-    return mk_app(mk_constant(get_tactic_notetac_name()),
+    return mk_app(mk_constant(get_tactic_note_tac_name()),
                   mk_constant(id), e);
 }
 
@@ -51,7 +51,7 @@ tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
 }
 
 void initialize_note_tactic() {
-    register_tac(get_tactic_notetac_name(),
+    register_tac(get_tactic_note_tac_name(),
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier");
                      check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression");