diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h
index d2040b09cd..5fb159e657 100644
--- a/src/frontends/lean/parser_config.h
+++ b/src/frontends/lean/parser_config.h
@@ -87,7 +87,7 @@ list<expr> get_mpz_notation(environment const & env, mpz const & n);
 /** \brief Return the notation declaration that start with a given head symbol.
 
     \remark Notation declarations that contain C++ and Lua actions are not indexed.
-    Thus, they are to included in the result.
+    Thus, they are not included in the result.
 */
 list<notation_entry> get_notation_entries(environment const & env, head_index const & idx);
 
diff --git a/src/library/tactic/algebraic_normalizer.cpp b/src/library/tactic/algebraic_normalizer.cpp
index 8feb74bb8b..1f0ed42535 100644
--- a/src/library/tactic/algebraic_normalizer.cpp
+++ b/src/library/tactic/algebraic_normalizer.cpp
@@ -63,7 +63,7 @@ void initialize_algebraic_normalizer() {
     register_trace_class("algebra");
 
     g_algebra = new name("algebra");
-    register_class_symbol_tracking_attribute(*g_algebra, "mark class whose instances are relevant for txhe algebraic normalizer");
+    register_class_symbol_tracking_attribute(*g_algebra, "mark class whose instances are relevant for the algebraic normalizer");
 
     DECLARE_VM_BUILTIN(name({"tactic", "trace_algebra_info"}), tactic_trace_algebra_info);
 }