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

fix(library/class_instance_resolution): uninitialized variables

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-27 15:34:08 -07:00
parent 20539d698f
commit 95348bc90b
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/class_instance_resolution.cpp
View file

@ -244,7 +244,10 @@ struct cienv {
m_next_local_idx(0),
m_next_uvar_idx(0),
m_next_mvar_idx(0),
m_multiple_instances(multiple_instances) {}
m_multiple_instances(multiple_instances),
m_max_depth(LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH),
m_trans_instances(LEAN_DEFAULT_CLASS_TRANS_INSTANCES),
m_trace_instances(LEAN_DEFAULT_CLASS_TRACE_INSTANCES) {}
bool is_not_reducible(name const & n) const {
return m_not_reducible_pred(n);
@ -288,14 +291,13 @@ struct cienv {
void set_options(options const & o) {
m_options = o;
if (m_trace_instances) {
m_options = m_options.update_if_undef(get_pp_purify_metavars_name(), false);
m_options = m_options.update_if_undef(get_pp_implicit_name(), true);
}
unsigned max_depth = get_class_instance_max_depth(o);
bool trans_instances = get_class_trans_instances(o);
bool trace_instances = get_class_trace_instances(o);
if (trace_instances) {
m_options = m_options.update_if_undef(get_pp_purify_metavars_name(), false);
m_options = m_options.update_if_undef(get_pp_implicit_name(), true);
}
if (m_max_depth != max_depth ||
m_trans_instances != trans_instances ||
m_trace_instances != trace_instances) {