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

fix(frontends/lean/elaborator): fix compilation with gcc

Browse source
This commit is contained in:
Gabriel Ebner 2017-05-19 20:42:21 +02:00 • committed by Leonardo de Moura
parent 8bd09fe282
commit dd91ef3b22
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -2627,7 +2627,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
<< S_fname << "'"
<< " was not provided, nor was it found in the source of type '"
<< src_S_name << "'."));
c_arg = mk_sorry({d}, ref);
c_arg = mk_sorry(some_expr(d), ref);
} else {
name base_S_name = *opt_base_S_name;
expr base_src = *mk_base_projections(m_env, src_S_name, base_S_name, *src);
@ -2646,7 +2646,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
msg += line() + format("but is expected to have type");
msg += std::get<2>(pp_data);
report_or_throw(elaborator_exception(ref, msg));
c_arg = mk_sorry({d}, ref);
c_arg = mk_sorry(some_expr(d), ref);
}
field2value.insert(S_fname, c_arg);
} else {
@ -2665,7 +2665,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
} else {
report_or_throw(elaborator_exception(e, sstream() << "invalid structure value { ... }, field '" <<
S_fname << "' was not provided"));
c_arg = mk_sorry({d}, ref);
c_arg = mk_sorry(some_expr(d), ref);
field2value.insert(S_fname, c_arg);
}
}