chore(util/sexpr/options): typos
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
0465c6ef53
commit
428d5cfb99
2 changed files with 2 additions and 2 deletions
|
@ -152,7 +152,7 @@ options join(options const & opts1, options const & opts2) {
|
|||
\brief Return a new set of options based on \c opts by adding the prefix \c prefix.
|
||||
|
||||
The procedure throws an exception if \c opts contains an options (o, v), s.t. prefix + o is
|
||||
an unknow option in Lean.
|
||||
an unknown option in Lean.
|
||||
*/
|
||||
options add_prefix(name const & prefix, options const & opts) {
|
||||
option_declarations const & decls = get_option_declarations();
|
||||
|
|
|
@ -66,7 +66,7 @@ public:
|
|||
\brief Return a new set of options based on \c opts by adding the prefix \c prefix.
|
||||
|
||||
The procedure throws an exception if \c opts contains an options (o, v), s.t. prefix + o is
|
||||
an unknow option in Lean.
|
||||
an unknown option in Lean.
|
||||
*/
|
||||
friend options add_prefix(name const & prefix, options const & opts);
|
||||
|
||||
|
|
Loading…
Reference in a new issue