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

fix(library/export): bug in --export-all option

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-30 17:23:38 -07:00
parent 9bf64c10fd
commit f264adfa92
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/export.cpp
View file

@ -194,8 +194,6 @@ class exporter {
} }
void export_definition(declaration const & d) { void export_definition(declaration const & d) {
if (inductive::is_intro_rule(m_env, d.get_name()) || inductive::is_elim_rule(m_env, d.get_name()))
return;
if (already_exported(d.get_name())) if (already_exported(d.get_name()))
return; return;
mark(d.get_name()); mark(d.get_name());
@ -216,6 +214,8 @@ class exporter {
} }
void export_axiom(declaration const & d) { void export_axiom(declaration const & d) {
if (inductive::is_intro_rule(m_env, d.get_name()) || inductive::is_elim_rule(m_env, d.get_name()))
return;
if (already_exported(d.get_name())) if (already_exported(d.get_name()))
return; return;
mark(d.get_name()); mark(d.get_name());