diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 5c6aacdb5..f846dac2e 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
 replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
-formatter.cpp definition.cpp replace_visitor.cpp environment.cpp
+formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp )
 
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 682f21b76..7ddaeb5cf 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -165,7 +165,7 @@ struct default_converter : public converter {
        D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field
        m_module_idx that is not none when this rule should be applied.
     */
-    bool is_opaque(definition const & d) const {
+    bool is_opaque(declaration const & d) const {
         lean_assert(d.is_definition());
         if (d.is_theorem()) return true;                                       // theorems are always opaque
         if (m_extra_opaque.contains(d.get_name())) return true;                // extra_opaque set overrides opaque flag
@@ -208,20 +208,20 @@ struct default_converter : public converter {
     }
 
     /** \brief Auxiliary method for \c is_delta */
-    optional<definition> is_delta_core(expr const & e) {
+    optional<declaration> is_delta_core(expr const & e) {
         if (is_constant(e)) {
             if (auto d = m_env.find(const_name(e)))
                 if (d->is_definition() && !is_opaque(*d))
                     return d;
         }
-        return none_definition();
+        return none_declaration();
     }
 
     /**
         \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
         to be expanded.
     */
-    optional<definition> is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); }
+    optional<declaration> is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); }
 
     /**
         \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
new file mode 100644
index 000000000..4142137d1
--- /dev/null
+++ b/src/kernel/declaration.cpp
@@ -0,0 +1,93 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/declaration.h"
+#include "kernel/environment.h"
+#include "kernel/for_each_fn.h"
+
+namespace lean {
+struct declaration::cell {
+    MK_LEAN_RC();
+    name              m_name;
+    level_param_names m_params;
+    expr              m_type;
+    bool              m_theorem;
+    optional<expr>    m_value;        // if none, then declaration is actually a postulate
+    // The following fields are only meaningful for definitions (which are not theorems)
+    unsigned          m_weight;
+    unsigned          m_module_idx;   // module idx where it was defined
+    bool              m_opaque;
+    // The following field affects the convertability checker.
+    // Let f be this definition, then if the following field is true,
+    // then whenever we are checking whether
+    //    (f a) is convertible to (f b)
+    // we will first check whether a is convertible to b.
+    // If the test fails, then we perform the full check.
+    bool              m_use_conv_opt;
+    void dealloc() { delete this; }
+
+    cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
+        m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
+        m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
+    cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
+         bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
+        m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
+        m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
+};
+
+declaration g_dummy = mk_axiom(name(), level_param_names(), expr());
+
+declaration::declaration():declaration(g_dummy) {}
+declaration::declaration(cell * ptr):m_ptr(ptr) {}
+declaration::declaration(declaration const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+declaration::declaration(declaration && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); }
+
+declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); }
+declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); }
+
+bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
+bool declaration::is_var_decl() const   { return !is_definition(); }
+bool declaration::is_axiom() const      { return is_var_decl() && m_ptr->m_theorem; }
+bool declaration::is_theorem() const    { return is_definition() && m_ptr->m_theorem; }
+
+name declaration::get_name() const { return m_ptr->m_name; }
+level_param_names const & declaration::get_params() const { return m_ptr->m_params; }
+expr declaration::get_type() const { return m_ptr->m_type; }
+
+bool declaration::is_opaque() const { return m_ptr->m_opaque; }
+expr declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
+unsigned declaration::get_weight() const { return m_ptr->m_weight; }
+module_idx declaration::get_module_idx() const { return m_ptr->m_module_idx; }
+bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
+
+declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
+                          bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
+    return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
+}
+declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
+                          bool opaque, module_idx mod_idx, bool use_conv_opt) {
+    unsigned w = 0;
+    for_each(v, [&](expr const & e, unsigned) {
+            if (is_constant(e)) {
+                auto d = env.find(const_name(e));
+                if (d && d->get_weight() > w)
+                    w = d->get_weight();
+            }
+            return true;
+        });
+    return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
+}
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
+    return declaration(new declaration::cell(n, params, t, true, v, true, 0, 0, false));
+}
+declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
+    return declaration(new declaration::cell(n, params, t, true));
+}
+declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
+    return declaration(new declaration::cell(n, params, t, false));
+}
+}
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
new file mode 100644
index 000000000..8bff7ce7b
--- /dev/null
+++ b/src/kernel/declaration.h
@@ -0,0 +1,90 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <algorithm>
+#include <string>
+#include "util/rc.h"
+#include "kernel/expr.h"
+
+namespace lean {
+/**
+    \brief Module index. The kernel provides only basic support
+    for implementing a module system outside of the kernel.
+
+    We need at least the notion of module index in the kernel, because
+    it affects the convertability procedure.
+
+    Given an opaque definition (non-theorem) d in module m1, then d is considered
+    to be transparent for any other opaque definition in module m1.
+*/
+typedef unsigned module_idx;
+
+/**
+   \brief Environment definitions, theorems, axioms and variable declarations.
+*/
+class declaration {
+    struct cell;
+    cell * m_ptr;
+    explicit declaration(cell * ptr);
+    friend struct cell;
+public:
+    /**
+       \brief The default constructor creates a reference to a "dummy"
+       declaration.  The actual "dummy" declaration is not relevant, and
+       no procedure should rely on the kind of declaration used.
+
+       We have a default constructor because some collections only work
+       with types that have a default constructor.
+    */
+    declaration();
+    declaration(declaration const & s);
+    declaration(declaration && s);
+    ~declaration();
+
+    friend void swap(declaration & a, declaration & b) { std::swap(a.m_ptr, b.m_ptr); }
+
+    declaration & operator=(declaration const & s);
+    declaration & operator=(declaration && s);
+
+    friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.m_ptr == d2.m_ptr; }
+
+    bool is_definition() const;
+    bool is_axiom() const;
+    bool is_theorem() const;
+    bool is_var_decl() const;
+
+    name get_name() const;
+    level_param_names const & get_params() const;
+    expr get_type() const;
+
+    expr get_value() const;
+    bool is_opaque() const;
+    unsigned get_weight() const;
+    module_idx get_module_idx() const;
+    bool use_conv_opt() const;
+
+    friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
+                                    expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
+    friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
+                                    unsigned weight, module_idx mod_idx, bool use_conv_opt);
+    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+    friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
+    friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
+};
+
+inline optional<declaration> none_declaration() { return optional<declaration>(); }
+inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
+inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
+
+declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
+                         bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
+declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
+                         bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
+declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
+}
diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp
deleted file mode 100644
index 08e9479ed..000000000
--- a/src/kernel/definition.cpp
+++ /dev/null
@@ -1,93 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/definition.h"
-#include "kernel/environment.h"
-#include "kernel/for_each_fn.h"
-
-namespace lean {
-struct definition::cell {
-    MK_LEAN_RC();
-    name              m_name;
-    level_param_names m_params;
-    expr              m_type;
-    bool              m_theorem;
-    optional<expr>    m_value;        // if none, then definition is actually a postulate
-    // The following fields are only meaningful for definitions (which are not theorems)
-    unsigned          m_weight;
-    unsigned          m_module_idx;   // module idx where it was defined
-    bool              m_opaque;
-    // The following field affects the convertability checker.
-    // Let f be this definition, then if the following field is true,
-    // then whenever we are checking whether
-    //    (f a) is convertible to (f b)
-    // we will first check whether a is convertible to b.
-    // If the test fails, then we perform the full check.
-    bool              m_use_conv_opt;
-    void dealloc() { delete this; }
-
-    cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
-        m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
-        m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
-    cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
-         bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
-        m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
-        m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
-};
-
-definition g_dummy = mk_axiom(name(), level_param_names(), expr());
-
-definition::definition():definition(g_dummy) {}
-definition::definition(cell * ptr):m_ptr(ptr) {}
-definition::definition(definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-definition::definition(definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-definition::~definition() { if (m_ptr) m_ptr->dec_ref(); }
-
-definition & definition::operator=(definition const & s) { LEAN_COPY_REF(s); }
-definition & definition::operator=(definition && s) { LEAN_MOVE_REF(s); }
-
-bool definition::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
-bool definition::is_var_decl() const   { return !is_definition(); }
-bool definition::is_axiom() const      { return is_var_decl() && m_ptr->m_theorem; }
-bool definition::is_theorem() const    { return is_definition() && m_ptr->m_theorem; }
-
-name definition::get_name() const { return m_ptr->m_name; }
-level_param_names const & definition::get_params() const { return m_ptr->m_params; }
-expr definition::get_type() const { return m_ptr->m_type; }
-
-bool definition::is_opaque() const { return m_ptr->m_opaque; }
-expr definition::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
-unsigned definition::get_weight() const { return m_ptr->m_weight; }
-module_idx definition::get_module_idx() const { return m_ptr->m_module_idx; }
-bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
-
-definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
-    return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
-}
-definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque, module_idx mod_idx, bool use_conv_opt) {
-    unsigned w = 0;
-    for_each(v, [&](expr const & e, unsigned) {
-            if (is_constant(e)) {
-                auto d = env.find(const_name(e));
-                if (d && d->get_weight() > w)
-                    w = d->get_weight();
-            }
-            return true;
-        });
-    return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
-}
-definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    return definition(new definition::cell(n, params, t, true, v, true, 0, 0, false));
-}
-definition mk_axiom(name const & n, level_param_names const & params, expr const & t) {
-    return definition(new definition::cell(n, params, t, true));
-}
-definition mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
-    return definition(new definition::cell(n, params, t, false));
-}
-}
diff --git a/src/kernel/definition.h b/src/kernel/definition.h
deleted file mode 100644
index fbc283e07..000000000
--- a/src/kernel/definition.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <algorithm>
-#include <string>
-#include "util/rc.h"
-#include "kernel/expr.h"
-
-namespace lean {
-/**
-    \brief Module index. The kernel provides only basic support
-    for implementing a module system outside of the kernel.
-
-    We need at least the notion of module index in the kernel, because
-    it affects the convertability procedure.
-
-    Given an opaque definition (non-theorem) d in module m1, then d is considered
-    to be transparent for any other opaque definition in module m1.
-*/
-typedef unsigned module_idx;
-
-/**
-   \brief Environment definitions, theorems, axioms and variable declarations.
-*/
-class definition {
-    struct cell;
-    cell * m_ptr;
-    explicit definition(cell * ptr);
-    friend struct cell;
-public:
-    /**
-       \brief The default constructor creates a reference to a "dummy"
-       definition.  The actual "dummy" definition is not relevant, and
-       no procedure should rely on the kind of definition used.
-
-       We have a default constructor because some collections only work
-       with types that have a default constructor.
-    */
-    definition();
-    definition(definition const & s);
-    definition(definition && s);
-    ~definition();
-
-    friend void swap(definition & a, definition & b) { std::swap(a.m_ptr, b.m_ptr); }
-
-    definition & operator=(definition const & s);
-    definition & operator=(definition && s);
-
-    friend bool is_eqp(definition const & d1, definition const & d2) { return d1.m_ptr == d2.m_ptr; }
-
-    bool is_definition() const;
-    bool is_axiom() const;
-    bool is_theorem() const;
-    bool is_var_decl() const;
-
-    name get_name() const;
-    level_param_names const & get_params() const;
-    expr get_type() const;
-
-    expr get_value() const;
-    bool is_opaque() const;
-    unsigned get_weight() const;
-    module_idx get_module_idx() const;
-    bool use_conv_opt() const;
-
-    friend definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
-                                    expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
-    friend definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
-                                    unsigned weight, module_idx mod_idx, bool use_conv_opt);
-    friend definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
-    friend definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
-    friend definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
-};
-
-inline optional<definition> none_definition() { return optional<definition>(); }
-inline optional<definition> some_definition(definition const & o) { return optional<definition>(o); }
-inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(o)); }
-
-definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
-definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
-definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
-definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
-definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
-}
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 485b8b696..c55110c03 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -44,8 +44,8 @@ bool environment_id::is_descendant(environment_id const & id) const {
     return false;
 }
 
-environment::environment(header const & h, environment_id const & ancestor, definitions const & d, name_set const & g, extensions const & exts):
-    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_global_levels(g), m_extensions(exts) {}
+environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts):
+    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {}
 
 environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel):
     environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
@@ -59,13 +59,13 @@ environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bo
 
 environment::~environment() {}
 
-optional<definition> environment::find(name const & n) const {
-    definition const * r = m_definitions.find(n);
-    return r ? some_definition(*r) : none_definition();
+optional<declaration> environment::find(name const & n) const {
+    declaration const * r = m_declarations.find(n);
+    return r ? some_declaration(*r) : none_declaration();
 }
 
-definition environment::get(name const & n) const {
-    definition const * r = m_definitions.find(n);
+declaration environment::get(name const & n) const {
+    declaration const * r = m_declarations.find(n);
     if (!r)
         throw_unknown_declaration(*this, n);
     return *r;
@@ -75,44 +75,44 @@ definition environment::get(name const & n) const {
     throw_kernel_exception(env, "invalid declaration, it was checked/certified in an incompatible environment");
 }
 
-environment environment::add(certified_definition const & d) const {
+environment environment::add(certified_declaration const & d) const {
     if (!m_id.is_descendant(d.get_id()))
         throw_incompatible_environment(*this);
-    name const & n = d.get_definition().get_name();
+    name const & n = d.get_declaration().get_name();
     if (find(n))
         throw_already_declared(*this, n);
-    return environment(m_header, m_id, insert(m_definitions, n, d.get_definition()), m_global_levels, m_extensions);
+    return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_global_levels, m_extensions);
 }
 
 environment environment::add_global_level(name const & n) const {
     if (m_global_levels.contains(n))
         throw_kernel_exception(*this,
                                "invalid global universe level declaration, environment already contains a universe level with the given name");
-    return environment(m_header, m_id, m_definitions, insert(m_global_levels, n), m_extensions);
+    return environment(m_header, m_id, m_declarations, insert(m_global_levels, n), m_extensions);
 }
 
 bool environment::is_global_level(name const & n) const {
     return m_global_levels.contains(n);
 }
 
-environment environment::replace(certified_definition const & t) const {
+environment environment::replace(certified_declaration const & t) const {
     if (!m_id.is_descendant(t.get_id()))
         throw_incompatible_environment(*this);
-    name const & n = t.get_definition().get_name();
+    name const & n = t.get_declaration().get_name();
     auto ax = find(n);
     if (!ax)
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the environment does not have an axiom with the given name");
     if (!ax->is_axiom())
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the current declaration in the environment is not an axiom");
-    if (!t.get_definition().is_theorem())
+    if (!t.get_declaration().is_theorem())
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the new declaration is not a theorem");
-    if (ax->get_type() != t.get_definition().get_type())
+    if (ax->get_type() != t.get_declaration().get_type())
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type");
-    return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_global_levels, m_extensions);
+    return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_global_levels, m_extensions);
 }
 
 environment environment::forget() const {
-    return environment(m_header, environment_id(), m_definitions, m_global_levels, m_extensions);
+    return environment(m_header, environment_id(), m_declarations, m_global_levels, m_extensions);
 }
 
 class extension_manager {
@@ -165,10 +165,10 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
     if (id >= new_exts->size())
         new_exts->resize(id+1);
     (*new_exts)[id] = ext;
-    return environment(m_header, m_id, m_definitions, m_global_levels, new_exts);
+    return environment(m_header, m_id, m_declarations, m_global_levels, new_exts);
 }
 
-void environment::for_each(std::function<void(definition const & d)> const & f) const {
-    m_definitions.for_each([&](name const &, definition const & d) { return f(d); });
+void environment::for_each(std::function<void(declaration const & d)> const & f) const {
+    m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
 }
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 8d3c290fd..11bd09bdb 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -15,12 +15,12 @@ Author: Leonardo de Moura
 #include "util/name_set.h"
 #include "kernel/expr.h"
 #include "kernel/constraint.h"
-#include "kernel/definition.h"
+#include "kernel/declaration.h"
 
 namespace lean {
 class type_checker;
 class environment;
-class certified_definition;
+class certified_declaration;
 
 /**
    \brief The Lean kernel can be instantiated with different normalization extensions.
@@ -98,16 +98,16 @@ public:
 */
 class environment {
     typedef std::shared_ptr<environment_header const>     header;
-    typedef rb_map<name, definition, name_quick_cmp>      definitions;
+    typedef rb_map<name, declaration, name_quick_cmp>     declarations;
     typedef std::shared_ptr<environment_extensions const> extensions;
 
     header         m_header;
     environment_id m_id;
-    definitions    m_definitions;
+    declarations   m_declarations;
     name_set       m_global_levels;
     extensions     m_extensions;
 
-    environment(header const & h, environment_id const & id, definitions const & d, name_set const & global_levels, extensions const & ext);
+    environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext);
 
 public:
     environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true,
@@ -140,11 +140,11 @@ public:
     /** \brief Return reference to the normalizer extension associatied with this environment. */
     normalizer_extension const & norm_ext() const { return m_header->norm_ext(); }
 
-    /** \brief Return definition with name \c n (if it is defined in this environment). */
-    optional<definition> find(name const & n) const;
+    /** \brief Return declaration with name \c n (if it is defined in this environment). */
+    optional<declaration> find(name const & n) const;
 
-    /** \brief Return definition with name \c n. Throws and exception if definition does not exist in this environment. */
-    definition get(name const & n) const;
+    /** \brief Return declaration with name \c n. Throws and exception if declaration does not exist in this environment. */
+    declaration get(name const & n) const;
 
     /**
         \brief Add a new global universe level with name \c n
@@ -156,20 +156,20 @@ public:
     bool is_global_level(name const & n) const;
 
     /**
-       \brief Extends the current environment with the given (certified) definition
+       \brief Extends the current environment with the given (certified) declaration
        This method throws an exception if:
-          - The definition was certified in an environment which is not an ancestor of this one.
-          - The environment already contains a definition with the given name.
+          - The declaration was certified in an environment which is not an ancestor of this one.
+          - The environment already contains a declaration with the given name.
     */
-    environment add(certified_definition const & d) const;
+    environment add(certified_declaration const & d) const;
 
     /**
-       \brief Replace the axiom with name <tt>t.get_definition().get_name()</tt> with the theorem t.get_definition().
+       \brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
        This method throws an exception if:
           - The theorem was certified in an environment which is not an ancestor of this one.
-          - The environment does not contain an axiom named <tt>t.get_definition().get_name()</tt>
+          - The environment does not contain an axiom named <tt>t.get_declaration().get_name()</tt>
     */
-    environment replace(certified_definition const & t) const;
+    environment replace(certified_declaration const & t) const;
 
     /**
        \brief Register an environment extension. Every environment
@@ -197,24 +197,24 @@ public:
     */
     environment forget() const;
 
-    /** \brief Apply the function \c f to each definition */
-    void for_each(std::function<void(definition const & d)> const & f) const;
+    /** \brief Apply the function \c f to each declaration */
+    void for_each(std::function<void(declaration const & d)> const & f) const;
 };
 
 class name_generator;
 
 /**
-   \brief A certified definition is one that has been type checked.
-   Only the type_checker class can create certified definitions.
+   \brief A certified declaration is one that has been type checked.
+   Only the type_checker class can create certified declarations.
 */
-class certified_definition {
-    friend certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize);
+class certified_declaration {
+    friend certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize);
     environment_id m_id;
-    definition     m_definition;
-    certified_definition(environment_id const & id, definition const & d):m_id(id), m_definition(d) {}
+    declaration    m_declaration;
+    certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}
 public:
-    /** \brief Return the id of the environment that was used to type check this definition. */
+    /** \brief Return the id of the environment that was used to type check this declaration. */
     environment_id const & get_id() const { return m_id; }
-    definition const & get_definition() const { return m_definition; }
+    declaration const & get_declaration() const { return m_declaration; }
 };
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 77dc351de..401fc5220 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -307,7 +307,7 @@ struct type_checker::imp {
             r = mk_sort(mk_succ(sort_level(e)));
             break;
         case expr_kind::Constant: {
-            definition d    = m_env.get(const_name(e));
+            declaration d    = m_env.get(const_name(e));
             auto const & ps = d.get_params();
             auto const & ls = const_levels(e);
             if (length(ps) != length(ls))
@@ -445,7 +445,7 @@ static void check_name(environment const & env, name const & n) {
         throw_already_declared(env, n);
 }
 
-certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
+certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
     check_no_mlocal(env, d.get_type());
     if (d.is_definition())
         check_no_mlocal(env, d.get_value());
@@ -466,10 +466,10 @@ certified_definition check(environment const & env, definition const & d, name_g
                                    });
         }
     }
-    return certified_definition(env.get_id(), d);
+    return certified_declaration(env.get_id(), d);
 }
 
-certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque, bool memoize) {
+certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque, bool memoize) {
     return check(env, d, name_generator(g_tmp_prefix), extra_opaque, memoize);
 }
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 8d9174ee4..74864057e 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -101,10 +101,10 @@ public:
 };
 
 /**
-   \brief Type check the given definition, and return a certified definition if it is type correct.
-   Throw an exception if the definition is type incorrect.
+   \brief Type check the given declaration, and return a certified declaration if it is type correct.
+   Throw an exception if the declaration is type incorrect.
 */
-certified_definition check(environment const & env, definition const & d,
-                           name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
-certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
+certified_declaration check(environment const & env, declaration const & d,
+                            name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
+certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
 }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 36c442489..f3b8d5b11 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -830,25 +830,25 @@ static void open_macro_definition(lua_State * L) {
     SET_GLOBAL_FUN(macro_definition_pred, "is_macro_definition");
 }
 
-// definition
-DECL_UDATA(definition)
-int push_optional_definition(lua_State * L, optional<definition> const & e) {  return e ? push_definition(L, *e) : push_nil(L); }
-#define DEFINITION_PRED(P) static int definition_ ## P(lua_State * L) {  return push_boolean(L, to_definition(L, 1).P()); }
-DEFINITION_PRED(is_definition)
-DEFINITION_PRED(is_theorem)
-DEFINITION_PRED(is_axiom)
-DEFINITION_PRED(is_var_decl)
-DEFINITION_PRED(is_opaque)
-DEFINITION_PRED(use_conv_opt)
-static int definition_get_name(lua_State * L) { return push_name(L, to_definition(L, 1).get_name()); }
-static int definition_get_params(lua_State * L) { return push_list_name(L, to_definition(L, 1).get_params()); }
-static int definition_get_type(lua_State * L) { return push_expr(L, to_definition(L, 1).get_type()); }
-static int definition_get_value(lua_State * L) {
-    if (to_definition(L, 1).is_definition())
-        return push_expr(L, to_definition(L, 1).get_value());
-    throw exception("arg #1 must be a definition");
+// declaration
+DECL_UDATA(declaration)
+int push_optional_declaration(lua_State * L, optional<declaration> const & e) {  return e ? push_declaration(L, *e) : push_nil(L); }
+#define DECLARATION_PRED(P) static int declaration_ ## P(lua_State * L) {  return push_boolean(L, to_declaration(L, 1).P()); }
+DECLARATION_PRED(is_definition)
+DECLARATION_PRED(is_theorem)
+DECLARATION_PRED(is_axiom)
+DECLARATION_PRED(is_var_decl)
+DECLARATION_PRED(is_opaque)
+DECLARATION_PRED(use_conv_opt)
+static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); }
+static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_params()); }
+static int declaration_get_type(lua_State * L) { return push_expr(L, to_declaration(L, 1).get_type()); }
+static int declaration_get_value(lua_State * L) {
+    if (to_declaration(L, 1).is_definition())
+        return push_expr(L, to_declaration(L, 1).get_value());
+    throw exception("arg #1 must be a declaration");
 }
-static int definition_get_weight(lua_State * L) { return push_integer(L, to_definition(L, 1).get_weight()); }
+static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
 static list<name> to_level_param_names(lua_State * L, int _idx) {
     return table_to_list<name>(L, _idx, [](lua_State * L, int idx) -> name {
             if (is_level(L, idx)) {
@@ -864,27 +864,27 @@ static list<name> to_level_param_names(lua_State * L, int _idx) {
             }
         });
 }
-static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_definition(L, 1).get_module_idx()); }
+static int declaration_get_module_idx(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_module_idx()); }
 static int mk_var_decl(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        return push_definition(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
+        return push_declaration(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
     else
-        return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
+        return push_declaration(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
 }
 static int mk_axiom(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        return push_definition(L, mk_axiom(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
+        return push_declaration(L, mk_axiom(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
     else
-        return push_definition(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
+        return push_declaration(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
 }
 static int mk_theorem(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 3)
-        return push_definition(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
+        return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
     else
-        return push_definition(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
+        return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
 }
 static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
     opaque       = get_bool_named_param(L, idx, "opaque", opaque);
@@ -896,60 +896,60 @@ static int mk_definition(lua_State * L) {
     int nargs = lua_gettop(L);
     bool opaque = true; unsigned weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true;
     if (nargs < 3) {
-        throw exception("mk_definition must have at least 3 arguments");
+        throw exception("mk_declaration must have at least 3 arguments");
     } else if (is_environment(L, 1)) {
         if (nargs < 4) {
-            throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
+            throw exception("mk_declaration must have at least 4 arguments, when the first argument is an environment");
         } else if (is_expr(L, 3)) {
             get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
-            return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
+            return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
                                                     to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
         } else {
             get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
-            return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
+            return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
                                                     to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
         }
     } else {
         if (is_expr(L, 2)) {
             get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
-            return push_definition(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
+            return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
                                                     to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
         } else {
             get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
-            return push_definition(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
+            return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
                                                     to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
         }
     }
 }
 
-static const struct luaL_Reg definition_m[] = {
-    {"__gc",             definition_gc}, // never throws
-    {"is_definition",    safe_function<definition_is_definition>},
-    {"is_theorem",       safe_function<definition_is_theorem>},
-    {"is_axiom",         safe_function<definition_is_axiom>},
-    {"is_var_decl",      safe_function<definition_is_var_decl>},
-    {"opaque",           safe_function<definition_is_opaque>},
-    {"use_conv_opt",     safe_function<definition_use_conv_opt>},
-    {"name",             safe_function<definition_get_name>},
-    {"univ_params",      safe_function<definition_get_params>},
-    {"type",             safe_function<definition_get_type>},
-    {"value",            safe_function<definition_get_value>},
-    {"weight",           safe_function<definition_get_weight>},
-    {"module_idx",       safe_function<definition_get_module_idx>},
+static const struct luaL_Reg declaration_m[] = {
+    {"__gc",             declaration_gc}, // never throws
+    {"is_definition",    safe_function<declaration_is_definition>},
+    {"is_theorem",       safe_function<declaration_is_theorem>},
+    {"is_axiom",         safe_function<declaration_is_axiom>},
+    {"is_var_decl",      safe_function<declaration_is_var_decl>},
+    {"opaque",           safe_function<declaration_is_opaque>},
+    {"use_conv_opt",     safe_function<declaration_use_conv_opt>},
+    {"name",             safe_function<declaration_get_name>},
+    {"univ_params",      safe_function<declaration_get_params>},
+    {"type",             safe_function<declaration_get_type>},
+    {"value",            safe_function<declaration_get_value>},
+    {"weight",           safe_function<declaration_get_weight>},
+    {"module_idx",       safe_function<declaration_get_module_idx>},
     {0, 0}
 };
 
-static void open_definition(lua_State * L) {
-    luaL_newmetatable(L, definition_mt);
+static void open_declaration(lua_State * L) {
+    luaL_newmetatable(L, declaration_mt);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
-    setfuncs(L, definition_m, 0);
+    setfuncs(L, declaration_m, 0);
 
-    SET_GLOBAL_FUN(definition_pred, "is_definition");
-    SET_GLOBAL_FUN(mk_var_decl,     "mk_var_decl");
-    SET_GLOBAL_FUN(mk_axiom,        "mk_axiom");
-    SET_GLOBAL_FUN(mk_theorem,      "mk_theorem");
-    SET_GLOBAL_FUN(mk_definition,   "mk_definition");
+    SET_GLOBAL_FUN(declaration_pred, "is_declaration");
+    SET_GLOBAL_FUN(mk_var_decl,      "mk_var_decl");
+    SET_GLOBAL_FUN(mk_axiom,         "mk_axiom");
+    SET_GLOBAL_FUN(mk_theorem,       "mk_theorem");
+    SET_GLOBAL_FUN(mk_definition,    "mk_definition");
 }
 
 // Formatter
@@ -1059,33 +1059,33 @@ static void open_environment_id(lua_State * L) {
     SET_GLOBAL_FUN(environment_id_pred, "is_environment_id");
 }
 
-// certified_definition
-DECL_UDATA(certified_definition)
-static int certified_definition_get_definition(lua_State * L) { return push_definition(L, to_certified_definition(L, 1).get_definition()); }
-static int certified_definition_get_id(lua_State * L) { return push_environment_id(L, to_certified_definition(L, 1). get_id()); }
+// certified_declaration
+DECL_UDATA(certified_declaration)
+static int certified_declaration_get_declaration(lua_State * L) { return push_declaration(L, to_certified_declaration(L, 1).get_declaration()); }
+static int certified_declaration_get_id(lua_State * L) { return push_environment_id(L, to_certified_declaration(L, 1). get_id()); }
 
-static const struct luaL_Reg certified_definition_m[] = {
-    {"__gc",             certified_definition_gc}, // never throws
-    {"definition",       safe_function<certified_definition_get_definition>},
-    {"environment_id",   safe_function<certified_definition_get_id>},
+static const struct luaL_Reg certified_declaration_m[] = {
+    {"__gc",             certified_declaration_gc}, // never throws
+    {"declaration",       safe_function<certified_declaration_get_declaration>},
+    {"environment_id",   safe_function<certified_declaration_get_id>},
     {0, 0}
 };
 
-static void certified_definition_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_certified_definition(tgt, to_certified_definition(src, i));
+static void certified_declaration_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_certified_declaration(tgt, to_certified_declaration(src, i));
 }
 
-static void open_certified_definition(lua_State * L) {
-    luaL_newmetatable(L, certified_definition_mt);
-    set_migrate_fn_field(L, -1, certified_definition_migrate);
+static void open_certified_declaration(lua_State * L) {
+    luaL_newmetatable(L, certified_declaration_mt);
+    set_migrate_fn_field(L, -1, certified_declaration_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
-    setfuncs(L, certified_definition_m, 0);
+    setfuncs(L, certified_declaration_m, 0);
 
-    SET_GLOBAL_FUN(certified_definition_pred, "is_certified_definition");
+    SET_GLOBAL_FUN(certified_declaration_pred, "is_certified_declaration");
 }
-static bool operator!=(certified_definition const &, certified_definition const &) { return true; }
-DEFINE_LUA_LIST(certified_definition, push_certified_definition, to_certified_definition)
+static bool operator!=(certified_declaration const &, certified_declaration const &) { return true; }
+DEFINE_LUA_LIST(certified_declaration, push_certified_declaration, to_certified_declaration)
 
 // Environment
 DECL_UDATA(environment)
@@ -1097,10 +1097,10 @@ static int environment_eta(lua_State * L) { return push_boolean(L, to_environmen
 static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
 static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
 static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); }
-static int environment_find(lua_State * L) { return push_optional_definition(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
-static int environment_get(lua_State * L) { return push_definition(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
-static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
-static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); }
+static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
+static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
+static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_declaration(L, 2))); }
+static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_declaration(L, 2))); }
 static int mk_empty_environment(lua_State * L) {
     unsigned trust_lvl    = get_uint_named_param(L, 1, "trust_lvl", 0);
     trust_lvl             = get_uint_named_param(L, 1, "trust_level", trust_lvl);
@@ -1125,9 +1125,9 @@ static int environment_type_check(lua_State * L) { return push_expr(L, type_chec
 static int environment_for_each(lua_State * L) {
     environment const & env = to_environment(L, 1);
     luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
-    env.for_each([&](definition const & d) {
+    env.for_each([&](declaration const & d) {
             lua_pushvalue(L, 2); // push user-fun
-            push_definition(L, d);
+            push_declaration(L, d);
             pcall(L, 1, 0, 0);
         });
     return 0;
@@ -1758,27 +1758,27 @@ static const struct luaL_Reg type_checker_ref_m[] = {
 static int type_check(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2)));
+        return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2)));
     else if (nargs == 3)
-        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3)));
+        return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3)));
     else if (nargs == 4)
-        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4)));
+        return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4)));
     else
-        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4),
+        return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4),
                                                   lua_toboolean(L, 5)));
 }
 
 static int add_declaration(lua_State * L) {
     int nargs = lua_gettop(L);
-    optional<certified_definition> d;
+    optional<certified_declaration> d;
     if (nargs == 2)
-        d = check(to_environment(L, 1), to_definition(L, 2));
+        d = check(to_environment(L, 1), to_declaration(L, 2));
     else if (nargs == 3)
-        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3));
+        d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3));
     else if (nargs == 4)
-        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
+        d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
     else
-        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
+        d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
     return push_environment(L, to_environment(L, 1).add(*d));
 }
 
@@ -1876,11 +1876,11 @@ void open_kernel_module(lua_State * L) {
     open_expr(L);
     open_list_expr(L);
     open_macro_definition(L);
-    open_definition(L);
+    open_declaration(L);
     open_formatter(L);
     open_environment_id(L);
-    open_certified_definition(L);
-    open_list_certified_definition(L);
+    open_certified_declaration(L);
+    open_list_certified_declaration(L);
     open_environment(L);
     open_io_state(L);
     open_justification(L);
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 67ad60faa..a8c0dc602 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -7,11 +7,11 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
-#include "kernel/definition.h"
+#include "kernel/declaration.h"
 #include "library/max_sharing.h"
 #include "library/kernel_serializer.h"
 
-// Procedures for serializing and deserializing kernel objects (levels, exprs, definitions)
+// Procedures for serializing and deserializing kernel objects (levels, exprs, declarations)
 namespace lean {
 // Universe level serialization
 class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
@@ -254,10 +254,10 @@ expr read_expr(deserializer & d) {
     return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read();
 }
 
-// Definition serialization
+// Declaration serialization
 static serializer & operator<<(serializer & s, level_param_names const & ps) { return write_list<name>(s, ps); }
 static level_param_names read_level_params(deserializer & d) { return read_list<name>(d); }
-serializer & operator<<(serializer & s, definition const & d) {
+serializer & operator<<(serializer & s, declaration const & d) {
     char k = 0;
     if (d.is_definition()) {
         k |= 1;
@@ -277,7 +277,7 @@ serializer & operator<<(serializer & s, definition const & d) {
     return s;
 }
 
-definition read_definition(deserializer & d, unsigned module_idx) {
+declaration read_declaration(deserializer & d, unsigned module_idx) {
     char k               = d.read_char();
     bool has_value       = (k & 1) != 0;
     bool is_theorem      = (k & 8) != 0;
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
index 341181964..9dfaa1953 100644
--- a/src/library/kernel_serializer.h
+++ b/src/library/kernel_serializer.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "util/serializer.h"
-#include "kernel/definition.h"
+#include "kernel/declaration.h"
 
 namespace lean {
 serializer & operator<<(serializer & s, level const & l);
@@ -21,8 +21,8 @@ serializer & operator<<(serializer & s, expr const & e);
 expr read_expr(deserializer & d);
 inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
 
-serializer & operator<<(serializer & s, definition const & d);
-definition read_definition(deserializer & d, unsigned module_idx);
+serializer & operator<<(serializer & s, declaration const & d);
+declaration read_declaration(deserializer & d, unsigned module_idx);
 
 void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd);
 struct register_macro_deserializer_fn {
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 8857238c4..e78955821 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -13,52 +13,52 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 using namespace lean;
 
-static environment add_def(environment const & env, definition const & d) {
+static environment add_decl(environment const & env, declaration const & d) {
     auto cd = check(env, d, name_generator("test"));
     return env.add(cd);
 }
 
 static void tst1() {
     environment env1;
-    auto env2 = add_def(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
+    auto env2 = add_decl(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
     lean_assert(!env1.find("Bool"));
     lean_assert(env2.find("Bool"));
     lean_assert(env2.find("Bool")->get_value() == mk_Bool());
     try {
-        auto env3 = add_def(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
+        auto env3 = add_decl(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
         lean_unreachable();
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
     }
     try {
-        auto env4 = add_def(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool()));
+        auto env4 = add_decl(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool()));
         lean_unreachable();
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
     }
     try {
-        auto env5 = add_def(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
+        auto env5 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
         lean_unreachable();
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
     }
     try {
-        auto env6 = add_def(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
+        auto env6 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
         lean_unreachable();
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
     }
     try {
-        auto env7 = add_def(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool()));
+        auto env7 = add_decl(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool()));
         lean_unreachable();
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
     }
     expr A = Const("A");
     expr x = Const("x");
-    auto env3 = add_def(env2, mk_definition("id", level_param_names(),
-                                            Pi(A, mk_Type(), A >> A),
-                                            Fun({{A, mk_Type()}, {x, A}}, x)));
+    auto env3 = add_decl(env2, mk_definition("id", level_param_names(),
+                                             Pi(A, mk_Type(), A >> A),
+                                             Fun({{A, mk_Type()}, {x, A}}, x)));
     expr c  = mk_local("c", "c", Bool);
     expr id = Const("id");
     type_checker checker(env3, name_generator("tmp"));
@@ -73,18 +73,18 @@ static void tst1() {
 static void tst2() {
     environment env;
     name base("base");
-    env = add_def(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
+    env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
     expr x = Const("x");
     expr y = Const("y");
     for (unsigned i = 1; i <= 100; i++) {
         expr prev = Const(name(base, i-1));
-        env = add_def(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
-                                         Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
+        env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
+                                          Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
     }
     expr A = Const("A");
-    env = add_def(env, mk_definition("id", level_param_names(),
-                                     Pi(A, mk_Type(), A >> A),
-                                     Fun({{A, mk_Type()}, {x, A}}, x)));
+    env = add_decl(env, mk_definition("id", level_param_names(),
+                                      Pi(A, mk_Type(), A >> A),
+                                      Fun({{A, mk_Type()}, {x, A}}, x)));
     type_checker checker(env, name_generator("tmp"));
     expr f96 = Const(name(base, 96));
     expr f97 = Const(name(base, 97));
@@ -129,9 +129,9 @@ static void tst3() {
     expr A = Const("A");
     expr x = Const("x");
     expr id = Const("id");
-    env = add_def(env, mk_definition("id", level_param_names(),
-                                     Pi(A, mk_Type(), A >> A),
-                                     Fun({{A, mk_Type()}, {x, A}}, x)));
+    env = add_decl(env, mk_definition("id", level_param_names(),
+                                      Pi(A, mk_Type(), A >> A),
+                                      Fun({{A, mk_Type()}, {x, A}}, x)));
     expr mk = Const("mk");
     expr proj1 = Const("proj1");
     expr a = Const("a");
diff --git a/tests/lua/threads/th2.lua b/tests/lua/threads/th2.lua
index a0e742ec1..4eb2629d5 100644
--- a/tests/lua/threads/th2.lua
+++ b/tests/lua/threads/th2.lua
@@ -2,9 +2,9 @@ S1 = State()
 S2 = State()
 code = [[
   function f(env, prefix, num, type)
-      local r = list_certified_definition()
+      local r = list_certified_declaration()
       for i = 1, num do
-          r = list_certified_definition(type_check(env, mk_var_decl(prefix .. "_" .. i, type)), r)
+          r = list_certified_declaration(type_check(env, mk_var_decl(prefix .. "_" .. i, type)), r)
       end
       return r
   end