diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp
index a2c481a5e3..588525c190 100644
--- a/src/frontend/operator_info.cpp
+++ b/src/frontend/operator_info.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "rc.h"
 
 namespace lean {
-
+/** \brief Actual implementation of operator_info */
 struct operator_info::imp {
     void dealloc() { delete this;  }
     MK_LEAN_RC();
@@ -22,7 +22,7 @@ struct operator_info::imp {
         m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list<name>())) {}
 
     imp(unsigned num_parts, name const * parts, fixity f, unsigned p):
-        m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(it2list<name, name const *>(parts, parts + num_parts)) {
+        m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(copy_to_list<name const *, name>(parts, parts + num_parts)) {
         lean_assert(num_parts > 0);
     }
 
diff --git a/src/frontend/scanner.cpp b/src/frontend/scanner.cpp
index d735d5636e..ba52f1def2 100644
--- a/src/frontend/scanner.cpp
+++ b/src/frontend/scanner.cpp
@@ -24,6 +24,7 @@ static name g_eq_name("=");
 
 static char g_normalized[256];
 
+/** \brief Auxiliary class for initializing global variable \c g_normalized. */
 class init_normalized_table {
     void set(int i, char v) { g_normalized[static_cast<unsigned>(i)] = v; }
 public:
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 9beb98f58d..bc7f384a13 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -9,8 +9,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 /**
-   \brief Return unit if <tt>num_args == 0<\tt>, args[0] if <tt>num_args == 1<\tt>, and
-   <tt>(op args[0] (op args[1] (op ... )))<\tt>
+   \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
+   <tt>(op args[0] (op args[1] (op ... )))</tt>
 */
 expr mk_bin_op(expr const & op, expr const & unit, unsigned num_args, expr const * args);
 expr mk_bin_op(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
@@ -80,13 +80,13 @@ expr mk_not_fn();
 inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
 inline expr Not(expr const & e) { return mk_not(e); }
 
-/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool<\tt> */
+/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool</tt> */
 expr mk_forall_fn();
 /** \brief Return the term (Forall A P), where A is a type and P : A -> bool */
 inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
 inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
 
-/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool<\tt> */
+/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */
 expr mk_exists_fn();
 /** \brief Return the term (exists A P), where A is a type and P : A -> bool */
 inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index ef312f31ee..98083119bd 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -65,7 +65,6 @@ public:
     expr_kind kind() const { return static_cast<expr_kind>(m_kind); }
     unsigned  hash() const { return m_hash; }
 };
-
 /**
    \brief Exprs for encoding formulas/expressions, types and proofs.
 */
@@ -197,9 +196,7 @@ public:
     ~expr_type();
     level const & get_level() const { return m_level; }
 };
-/**
-   \brief Base class for semantic attachment cells.
-*/
+/** \brief Base class for semantic attachment cells. */
 class value {
     void dealloc() { delete this; }
     MK_LEAN_RC();
@@ -214,7 +211,6 @@ public:
     virtual format pp() const = 0;
     virtual unsigned hash() const = 0;
 };
-
 /** \brief Semantic attachments */
 class expr_value : public expr_cell {
     value & m_val;
@@ -332,9 +328,13 @@ inline name const &  let_name(expr_cell * e)             { return to_let(e)->get
 inline expr const &  let_value(expr_cell * e)            { return to_let(e)->get_value(); }
 inline expr const &  let_body(expr_cell * e)             { return to_let(e)->get_body(); }
 
+/** \brief Return the reference counter of the given expression. */
 inline unsigned      get_rc(expr const &  e)              { return e.raw()->get_rc(); }
+/** \brief Return true iff the reference counter of the given expression is greater than 1. */
 inline bool          is_shared(expr const & e)            { return get_rc(e) > 1; }
+/** \brief Return the de Bruijn index of the given expression. \pre is_var(e) */
 inline unsigned      var_idx(expr const & e)              { return to_var(e)->get_vidx(); }
+/** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */
 inline bool          is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr const & e)           { return to_constant(e)->get_name(); }
 inline value const & to_value(expr const & e)             { return to_value(e.raw()); }
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index f8cd87392f..9c80a278be 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -13,21 +13,25 @@ Author: Leonardo de Moura
 #include "hash.h"
 
 namespace lean {
+/** \brief Base class for representing universe level cells. */
 struct level_cell {
     void dealloc();
     MK_LEAN_RC()
     level_kind m_kind;
     level_cell(level_kind k):m_rc(1), m_kind(k) {}
 };
+/** \brief Cell for universe variables. */
 struct level_uvar : public level_cell {
     name m_name;
     level_uvar(name const & n):level_cell(level_kind::UVar), m_name(n) {}
 };
+/** \brief Cell for representing the universe <tt>l + k</tt>, where \c l is a level and \c k a unsigned integer. */
 struct level_lift : public level_cell {
     level    m_l;
     unsigned m_k;
     level_lift(level const & l, unsigned k):level_cell(level_kind::Lift), m_l(l), m_k(k) {}
 };
+/** \brief Cell for representing the universe <tt>max l_1 ... l_n</tt>, where <tt>n == m_size</tt>. */
 struct level_max : public level_cell {
     unsigned m_size;
     level    m_levels[0];
diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp
index 3dbf5ac356..0f00f5cd42 100644
--- a/src/kernel/occurs.cpp
+++ b/src/kernel/occurs.cpp
@@ -22,7 +22,10 @@ void for_each(F & f, context const * c, unsigned sz, expr const * es) {
         visitor(es[i]);
 }
 
-namespace occurs_ns { struct found {}; }
+namespace occurs_ns {
+/** \brief Auxiliary struct used to sign (as an exception) that an occurrence was found. */
+struct found {};
+}
 bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
     auto visitor = [&](expr const & e, unsigned offset) -> void {
         if (is_constant(e)) {
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index df8a475728..a54adf9612 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -43,6 +43,7 @@ bool is_convertible(expr const & expected, expr const & given, environment const
     return is_convertible_core(e_n, g_n, env);
 }
 
+/** \brief Auxiliary functional object used to implement infer_type. */
 struct infer_type_fn {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
 
diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp
index 07a333f132..196b0b43c0 100644
--- a/src/tests/util/list.cpp
+++ b/src/tests/util/list.cpp
@@ -24,7 +24,7 @@ static void tst1() {
 
 static void tst2() {
     std::vector<int> a{10, 20, 30};
-    list<int> l = it2list<int>(a.begin(), a.end());
+    list<int> l = copy_to_list(a.begin(), a.end());
     std::cout << l << "\n";
     lean_assert(head(l) == 10);
     lean_assert(head(tail(l)) == 20);
@@ -34,7 +34,7 @@ static void tst2() {
 
 static void tst3() {
     int a[3] = {10, 20, 30};
-    list<int> l = it2list<int, int*>(a, a+3);
+    list<int> l = copy_to_list<int*, int>(a, a+3);
     std::cout << l << "\n";
     lean_assert(head(l) == 10);
     lean_assert(head(tail(l)) == 20);
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 1d998eaa11..58287a7db1 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -10,7 +10,12 @@ Author: Leonardo de Moura
 #include "debug.h"
 
 namespace lean {
-
+/**
+    \brief Very similar to std::vector, but stores elements on the
+    system stack when collection has less than \c INITIAL_SIZE.
+    This collection is useful when writing functions that need
+    temporary storage.
+*/
 template<typename T, unsigned INITIAL_SIZE=16>
 class buffer {
 protected:
diff --git a/src/util/exception.h b/src/util/exception.h
index 6951dabe2d..93342ea422 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include <string>
 
 namespace lean {
-
+/** \brief Base class for all Lean exceptions */
 class exception : public std::exception {
 protected:
     std::string m_msg;
@@ -20,7 +20,7 @@ public:
     virtual ~exception() noexcept;
     virtual char const * what() const noexcept;
 };
-
+/** \brief Exception produced by a Lean parser. */
 class parser_exception : public exception {
 protected:
     unsigned m_line;
diff --git a/src/util/list.h b/src/util/list.h
index 85d24367cc..b6561c95fc 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -13,8 +13,6 @@ Author: Leonardo de Moura
 namespace lean {
 /**
    \brief Basic list template.
-
-   Remark: == is pointer equality.
 */
 template<typename T>
 class list {
@@ -66,6 +64,7 @@ public:
     }
     friend bool operator!=(list const & l1, list const & l2) { return !(l1 == l2); }
 
+    /** \brief List iterator object. */
     class iterator {
         friend class list;
         cell const * m_it;
@@ -119,7 +118,8 @@ template<typename T> unsigned length(list<T> const & l) {
     return r;
 }
 
-template<typename T, typename It> list<T> it2list(It const & begin, It const & end) {
+/** \brief Return a list containing the elements in the subrange <tt>[begin, end)</tt>. */
+template<typename It, typename T = typename It::value_type> list<T> copy_to_list(It const & begin, It const & end) {
     list<T> r;
     auto it = end;
     while (it != begin) {