From f264adfa9263a66f5c1c3a6b1fbcfa891ea7375b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jul 2015 17:23:38 -0700 Subject: [PATCH] fix(library/export): bug in --export-all option --- src/library/export.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/export.cpp b/src/library/export.cpp index 623b7fe1b..b03eafb5f 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -194,8 +194,6 @@ class exporter { } 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())) return; mark(d.get_name()); @@ -216,6 +214,8 @@ class exporter { } 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())) return; mark(d.get_name());