diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 514147ab8..c876949b4 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1607,14 +1607,7 @@ expr elaborator::visit_prenum(expr const & e, constraint_seq & cs) {
     lean_assert(is_prenum(e));
     mpz const & v  = prenum_value(e);
     tag e_tag      = e.get_tag();
-    // Remark: In HoTT mode, we only partially support the new encoding for numerals.
-    // We fix A to num, and we rely on coercions to cast them to other types.
-    // This is quite different from the approach used in the standard library
-    expr A;
-    // if (is_standard(env()))
-        A = m_full_context.mk_meta(m_ngen, none_expr(), e_tag);
-    // else
-    //     A = mk_constant(get_num_name()).set_tag(e_tag);
+    expr A = m_full_context.mk_meta(m_ngen, none_expr(), e_tag);
     level A_lvl = sort_level(m_tc->ensure_type(A, cs));
     levels ls(A_lvl);
     bool is_strict = true;
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index c46407517..33681dba9 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -42,12 +42,6 @@ static unsigned parse_precedence_core(parser & p) {
         return p.parse_small_nat();
     } else {
         environment env = p.env();
-        // if (!is_standard(env)) {
-        //     // TODO(Leo): remove this if we decide to implement
-        //     // arithmetical notation using type classes in the HoTT
-        //     // library.
-        //     env = open_num_notation(p.env());
-        // }
         env = open_prec_aliases(env);
         parser::local_scope scope(p, env);
         expr pre_val = p.parse_expr(get_max_prec());