michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(api/lean_univ): typo

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-18 16:01:50 -07:00
parent 858971c3a5
commit a18983c1aa
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/lean_univ.h
View file

@ -48,7 +48,7 @@ lean_bool lean_univ_mk_global(lean_name n, lean_univ * r, lean_exception * ex);
/** \brief Create a universe meta-variable with the given name. */
lean_bool lean_univ_mk_meta(lean_name n, lean_univ * r, lean_exception * ex);
/** \brief Store in \c r a string representation of the given options object.
/** \brief Store in \c r a string representation of the given universe object.
\remark \c r must be deleted using #lean_string_del */
lean_bool lean_univ_to_string(lean_univ u, char const ** r, lean_exception * ex);