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

fix(frontends/lean/elaborator): option name

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 14:03:47 +01:00
parent 1d16b5d2ad
commit c03ae24d22
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/frontends/lean/elaborator.cpp
View file

@ -40,7 +40,7 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
// ========================================== // ==========================================
// elaborator configuration options // elaborator configuration options
static name g_elaborator_local_instances{"lean", "elaborator", "local_instances"}; static name g_elaborator_local_instances{"elaborator", "local_instances"};
RegisterBoolOption(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances"); RegisterBoolOption(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances");
bool get_elaborator_local_instances(options const & opts) { bool get_elaborator_local_instances(options const & opts) {
return opts.get_bool(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES); return opts.get_bool(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);