max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): typos

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-30 17:08:07 +02:00 • committed by Leonardo de Moura
parent 59184e888f
commit be6f2eada7
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser_config.h
View file

@ -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);

2
src/library/tactic/algebraic_normalizer.cpp
View file

@ -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);
}