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

fix(kernel/declaration): typo and restoring trusted flag for constants

Browse source
This commit is contained in:
Leonardo de Moura 2016-04-28 15:59:09 -07:00
parent c14bee0bbd
commit 0b812bc91d
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/declaration.h
View file

@ -77,7 +77,7 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned w);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = false);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = true);
void initialize_declaration();
void finalize_declaration();

2
src/library/kernel_serializer.cpp
View file

@ -326,7 +326,7 @@ declaration read_declaration(deserializer & d) {
if (is_th_ax)
return mk_axiom(n, ps, t);
else
return mk_constant_assumption(n, ps, t);
return mk_constant_assumption(n, ps, t, is_trusted);
}
}