diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 046fa760a4..fdee1f1143 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -970,6 +970,8 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
     case expr_kind::Macro:     r = visit_macro(fn, expected_type, true); break;
     case expr_kind::Lambda:    r = visit_lambda(fn, expected_type); break;
     case expr_kind::Let:       r = visit_let(fn, expected_type); break;
+    case expr_kind::Quote:
+        throw elaborator_exception(ref, "invalid application, function expected");
     }
     save_identifier_info(r);
     if (has_args)
@@ -3654,6 +3656,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
                     return copy_pos(e, visit_app(e, expected_type));
                 case expr_kind::Let:
                     return copy_pos(e, visit_let(e, expected_type));
+                case expr_kind::Quote:
+                    return copy_pos(e, visit_expr_quote(e, expected_type));
             }
             lean_unreachable(); // LCOV_EXCL_LINE
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ad4790c9bf..bd09beadb3 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -309,6 +309,12 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
                 args.push_back(copy_with_new_pos(macro_arg(e, i), p));
             return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
         }
+    case expr_kind::Quote:
+        if (is_pexpr_quote(e)) {
+            return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
+        } else {
+            return save_pos(e, p);
+        }
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -1719,43 +1725,45 @@ struct to_pattern_fn {
 
 static expr quote(expr const & e) {
     switch (e.kind()) {
-        case expr_kind::BVar:
-            return mk_app(mk_constant({"expr", "bvar"}), quote(var_idx(e)));
-        case expr_kind::Sort:
-            return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
-        case expr_kind::Constant:
-            return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
-        case expr_kind::Meta:
+    case expr_kind::BVar:
+        return mk_app(mk_constant({"expr", "bvar"}), quote(var_idx(e)));
+    case expr_kind::Sort:
+        return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
+    case expr_kind::Constant:
+        return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
+    case expr_kind::Meta:
+        return mk_expr_placeholder();
+    case expr_kind::FVar:
+        throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
+                                   << mlocal_pp_name(e) << "'");
+    case expr_kind::App:
+        if (is_metavar_app(e)) {
+            /* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
+               by type_context::elim_mvar_deps when we create lambda/pi-expressions. */
             return mk_expr_placeholder();
-        case expr_kind::FVar:
-            throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
-                                                    << mlocal_pp_name(e) << "'");
-        case expr_kind::App:
-            if (is_metavar_app(e)) {
-                /* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
-                   by type_context::elim_mvar_deps when we create lambda/pi-expressions. */
-                return mk_expr_placeholder();
-            } else {
-                return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
-            }
-        case expr_kind::Lambda:
-            return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
-                          quote(binding_domain(e)), quote(binding_body(e)));
-        case expr_kind::Pi:
-            return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
-                          quote(binding_domain(e)), quote(binding_body(e)));
-        case expr_kind::Let:
-            return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
-                          quote(let_value(e)), quote(let_body(e)));
-        case expr_kind::Macro:
-            if (is_antiquote(e))
-                return get_antiquote_expr(e);
-            if (is_typed_expr(e))
-                return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
-            if (is_inaccessible(e))
-                return mk_expr_placeholder();
-            throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
-                                                    << macro_def(e).get_name() << "'");
+        } else {
+            return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
+        }
+    case expr_kind::Lambda:
+        return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
+                      quote(binding_domain(e)), quote(binding_body(e)));
+    case expr_kind::Pi:
+        return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
+                      quote(binding_domain(e)), quote(binding_body(e)));
+    case expr_kind::Let:
+        return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
+                      quote(let_value(e)), quote(let_body(e)));
+    case expr_kind::Macro:
+        if (is_antiquote(e))
+            return get_antiquote_expr(e);
+        if (is_typed_expr(e))
+            return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
+        if (is_inaccessible(e))
+            return mk_expr_placeholder();
+        throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
+                                   << macro_def(e).get_name() << "'");
+    case expr_kind::Quote:
+        throw elaborator_exception(e, sstream() << "invalid quotation, quote found");
     }
     lean_unreachable();
 }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 462b5b6c7f..062f86c267 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1781,6 +1781,11 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     case expr_kind::Pi:        return pp_pi(e);
     case expr_kind::Macro:     return pp_macro(e);
     case expr_kind::Let:       return pp_let(e);
+    case expr_kind::Quote:
+        if (quote_is_reflected(e))
+            return result(format("`(") + nest(4, pp(quote_value(e)).fmt()) + format(")"));
+        else
+            return result(format("``(") + nest(2, pp(quote_value(e)).fmt()) + format(")"));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index ae816bcf88..2247d0e5e9 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -107,6 +107,11 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
         }
         result = true;
         break;
+    case expr_kind::Quote:
+        if (quote_is_reflected(a) != quote_is_reflected(b) || quote_value(a) != quote_value(b))
+            return false;
+        result = true;
+        break;
     }
     if (result)
         merge(r1, r2);
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 7b0832183e..0e5f23b2a2 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -285,27 +285,6 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
     delete this;
 }
 
-// Macro definition
-bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; }
-bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); }
-unsigned macro_definition_cell::trust_level() const { return 0; }
-
-void macro_definition_cell::display(std::ostream & out) const { out << get_name(); }
-unsigned macro_definition_cell::hash() const { return get_name().hash(); }
-
-macro_definition::macro_definition(macro_definition_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
-macro_definition::macro_definition(macro_definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-macro_definition::macro_definition(macro_definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-macro_definition::~macro_definition() { if (m_ptr) m_ptr->dec_ref(); }
-macro_definition & macro_definition::operator=(macro_definition const & s) { LEAN_COPY_REF(s); }
-macro_definition & macro_definition::operator=(macro_definition && s) { LEAN_MOVE_REF(s); }
-bool macro_definition::operator<(macro_definition const & other) const {
-    if (get_name() == other.get_name())
-        return m_ptr->lt(*other.m_ptr);
-    else
-        return get_name() < other.get_name();
-}
-
 static unsigned add_weight(unsigned num, expr const * args) {
     unsigned r = 0;
     for (unsigned i = 0; i < num; i++)
@@ -323,44 +302,6 @@ static unsigned get_loose_bvar_range(unsigned num, expr const * args) {
     return r;
 }
 
-expr_macro::expr_macro(expr_macro const & src, expr const * new_args):
-    expr_composite(src),
-    m_definition(src.m_definition),
-    m_num_args(src.m_num_args) {
-    expr * data = get_args_ptr();
-    std::uninitialized_copy(new_args, new_args + m_num_args, data);
-}
-
-expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args):
-    expr_composite(expr_kind::Macro,
-                   lean::hash(num, [&](unsigned i) { return args[i].hash(); }, m.hash()),
-                   std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }),
-                   std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }),
-                   std::any_of(args, args+num, [](expr const & e) { return e.has_fvar(); }),
-                   std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
-                   inc_weight(add_weight(num, args)),
-                   get_loose_bvar_range(num, args)),
-    m_definition(m),
-    m_num_args(num) {
-    expr * data = get_args_ptr();
-    m_depth = 0;
-    for (unsigned i = 0; i < num; i++) {
-        unsigned d = get_depth(args[i]);
-        if (d > m_depth)
-            m_depth = d;
-    }
-    m_depth++;
-    std::uninitialized_copy(args, args + num, data);
-}
-void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
-    expr * args = get_args_ptr();
-    for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
-    this->~expr_macro();
-    char * mem = reinterpret_cast<char*>(this);
-    delete[] mem;
-}
-expr_macro::~expr_macro() {}
-
 // =======================================
 // Constructors
 
@@ -373,10 +314,6 @@ expr mk_fvar(name const & n) {
 expr mk_constant(name const & n, levels const & ls) {
     return expr(new expr_const(n, ls));
 }
-expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
-    char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
-    return expr(new (mem) expr_macro(m, num, args));
-}
 expr mk_metavar(name const & n, name const & pp_n, expr const & t) {
     return expr(new expr_mlocal(true, n, pp_n, t));
 }
@@ -415,7 +352,6 @@ void expr_cell::dealloc() {
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
             case expr_kind::BVar:       static_cast<expr_bvar*>(it)->dealloc(); break;
-            case expr_kind::Macro:      static_cast<expr_macro*>(it)->dealloc(todo); break;
             case expr_kind::Meta:       static_cast<expr_mlocal*>(it)->dealloc(todo); break;
             case expr_kind::FVar:       static_cast<expr_fvar*>(it)->dealloc(todo); break;
             case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(); break;
@@ -424,6 +360,9 @@ void expr_cell::dealloc() {
             case expr_kind::Lambda:
             case expr_kind::Pi:         static_cast<expr_binding*>(it)->dealloc(todo); break;
             case expr_kind::Let:        static_cast<expr_let*>(it)->dealloc(todo); break;
+
+            case expr_kind::Macro:      static_cast<expr_macro*>(it)->dealloc(todo); break;
+            case expr_kind::Quote:      static_cast<expr_quote*>(it)->dealloc(todo); break;
            }
         }
     } catch (std::bad_alloc&) {
@@ -539,9 +478,15 @@ unsigned get_weight(expr const & e) {
     case expr_kind::BVar:  case expr_kind::Constant: case expr_kind::Sort:
     case expr_kind::Meta: case expr_kind::FVar:
         return 1;
-    case expr_kind::Lambda: case expr_kind::Pi:  case expr_kind::Macro:
+    case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
         return static_cast<expr_composite*>(e.raw())->m_weight;
+
+
+    case expr_kind::Macro:
+        return static_cast<expr_composite*>(e.raw())->m_weight;
+    case expr_kind::Quote:
+        return 1;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -551,9 +496,15 @@ unsigned get_depth(expr const & e) {
     case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
     case expr_kind::Meta: case expr_kind::FVar:
         return 1;
-    case expr_kind::Lambda: case expr_kind::Pi:  case expr_kind::Macro:
+    case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
         return static_cast<expr_composite*>(e.raw())->m_depth;
+
+
+    case expr_kind::Macro:
+        return static_cast<expr_composite*>(e.raw())->m_depth;
+    case expr_kind::Quote:
+        return 1;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -613,19 +564,6 @@ expr update_constant(expr const & e, levels const & new_levels) {
         return e;
 }
 
-expr update_macro(expr const & e, unsigned num, expr const * args) {
-    if (num == macro_num_args(e)) {
-        unsigned i = 0;
-        for (i = 0; i < num; i++) {
-            if (!is_eqp(macro_arg(e, i), args[i]))
-                break;
-        }
-        if (i == num)
-            return e;
-    }
-    return mk_macro(to_macro(e)->m_definition, num, args);
-}
-
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) {
     if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body))
         return mk_let(let_name(e), new_type, new_value, new_body);
@@ -638,12 +576,16 @@ bool is_atomic(expr const & e) {
     case expr_kind::Constant: case expr_kind::Sort:
     case expr_kind::BVar:
         return true;
-    case expr_kind::Macro:
-        return to_macro(e)->get_num_args() == 0;
     case expr_kind::App:      case expr_kind::Meta:
     case expr_kind::FVar:     case expr_kind::Lambda:
     case expr_kind::Pi:       case expr_kind::Let:
         return false;
+
+
+    case expr_kind::Macro:
+        return to_macro(e)->get_num_args() == 0;
+    case expr_kind::Quote:
+        return true;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -798,8 +740,11 @@ std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
     case expr_kind::App:      out << "App"; break;
     case expr_kind::Lambda:   out << "Lambda"; break;
     case expr_kind::Pi:       out << "Pi"; break;
-    case expr_kind::Macro:    out << "Macro"; break;
     case expr_kind::Let:      out << "Let"; break;
+
+
+    case expr_kind::Macro:    out << "Macro"; break;
+    case expr_kind::Quote:    out << "Quote"; break;
     }
     return out;
 }
@@ -817,4 +762,98 @@ void finalize_expr() {
     delete g_dummy;
     delete g_default_name;
 }
+
+/* ================ LEGACY CODE ================ */
+
+// Macro definition
+bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; }
+bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); }
+unsigned macro_definition_cell::trust_level() const { return 0; }
+
+void macro_definition_cell::display(std::ostream & out) const { out << get_name(); }
+unsigned macro_definition_cell::hash() const { return get_name().hash(); }
+
+macro_definition::macro_definition(macro_definition_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
+macro_definition::macro_definition(macro_definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+macro_definition::macro_definition(macro_definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+macro_definition::~macro_definition() { if (m_ptr) m_ptr->dec_ref(); }
+macro_definition & macro_definition::operator=(macro_definition const & s) { LEAN_COPY_REF(s); }
+macro_definition & macro_definition::operator=(macro_definition && s) { LEAN_MOVE_REF(s); }
+bool macro_definition::operator<(macro_definition const & other) const {
+    if (get_name() == other.get_name())
+        return m_ptr->lt(*other.m_ptr);
+    else
+        return get_name() < other.get_name();
+}
+
+expr_macro::expr_macro(expr_macro const & src, expr const * new_args):
+    expr_composite(src),
+    m_definition(src.m_definition),
+    m_num_args(src.m_num_args) {
+    expr * data = get_args_ptr();
+    std::uninitialized_copy(new_args, new_args + m_num_args, data);
+}
+
+expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args):
+    expr_composite(expr_kind::Macro,
+                   lean::hash(num, [&](unsigned i) { return args[i].hash(); }, m.hash()),
+                   std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }),
+                   std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }),
+                   std::any_of(args, args+num, [](expr const & e) { return e.has_fvar(); }),
+                   std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
+                   inc_weight(add_weight(num, args)),
+                   get_loose_bvar_range(num, args)),
+    m_definition(m),
+    m_num_args(num) {
+    expr * data = get_args_ptr();
+    m_depth = 0;
+    for (unsigned i = 0; i < num; i++) {
+        unsigned d = get_depth(args[i]);
+        if (d > m_depth)
+            m_depth = d;
+    }
+    m_depth++;
+    std::uninitialized_copy(args, args + num, data);
+}
+void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
+    expr * args = get_args_ptr();
+    for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
+    this->~expr_macro();
+    char * mem = reinterpret_cast<char*>(this);
+    delete[] mem;
+}
+expr_macro::~expr_macro() {}
+
+expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
+    char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
+    return expr(new (mem) expr_macro(m, num, args));
+}
+
+expr update_macro(expr const & e, unsigned num, expr const * args) {
+    if (num == macro_num_args(e)) {
+        unsigned i = 0;
+        for (i = 0; i < num; i++) {
+            if (!is_eqp(macro_arg(e, i), args[i]))
+                break;
+        }
+        if (i == num)
+            return e;
+    }
+    return mk_macro(to_macro(e)->m_definition, num, args);
+}
+
+expr_quote::expr_quote(bool r, expr const & v):
+    expr_cell(expr_kind::Quote, v.hash(), false, false, false, false),
+    m_reflected(r),
+    m_value(v) {
+}
+
+void expr_quote::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_value, todelete);
+    delete this;
+}
+
+expr mk_quote(bool reflected, expr const & val) {
+    return expr(new expr_quote(reflected, val));
+}
 }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index e6b3536d05..7a8ca25a21 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -38,9 +38,13 @@ class expr;
           |   Lambda        name expr expr
           |   Pi            name expr expr
           |   Let           name expr expr expr
+
+          The following constructors will be deleted in the future
+
+          |   Quote         bool expr
           |   Macro         macro
 */
-enum class expr_kind { BVar, FVar, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro };
+enum class expr_kind { BVar, FVar, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro, Quote };
 class expr_cell {
 protected:
     // The bits of the following field mean:
@@ -128,8 +132,10 @@ public:
     friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
     friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
 
+    // TODO(Leo): delete
     friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
     friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
+    friend expr mk_quote(bool reflected, expr const & val);
 };
 
 SPECIALIZE_OPTIONAL_FOR_SMART_PTR(expr)
@@ -329,98 +335,13 @@ public:
     level const & get_level() const { return m_level; }
 };
 
-/** \brief Abstract class for macro_definitions */
-class macro_definition_cell {
-protected:
-    void dealloc() { delete this; }
-    MK_LEAN_RC();
-    /**
-       \brief Auxiliary method used for implementing a total order on macro
-       attachments. It is invoked by operator<, and it is only invoked when
-       <tt>get_name() == other.get_name()</tt>
-    */
-    virtual bool lt(macro_definition_cell const &) const;
-public:
-    macro_definition_cell():m_rc(0) {}
-    virtual ~macro_definition_cell() {}
-    virtual name get_name() const = 0;
-    virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const = 0;
-    virtual optional<expr> expand(expr const & m, abstract_type_context & ctx) const = 0;
-    virtual optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return expand(m, ctx); }
-    virtual unsigned trust_level() const;
-    virtual bool operator==(macro_definition_cell const & other) const;
-    virtual void display(std::ostream & out) const;
-    virtual unsigned hash() const;
-    virtual void write(serializer & s) const = 0;
-    typedef std::function<expr(deserializer&, unsigned, expr const *)> reader;
-};
-
-/** \brief Smart pointer for macro definitions */
-class macro_definition {
-public:
-    macro_definition_cell * m_ptr;
-public:
-    explicit macro_definition(macro_definition_cell * ptr);
-    macro_definition(macro_definition const & s);
-    macro_definition(macro_definition && s);
-    ~macro_definition();
-
-    macro_definition & operator=(macro_definition const & s);
-    macro_definition & operator=(macro_definition && s);
-
-    name get_name() const { return m_ptr->get_name(); }
-    expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
-        return m_ptr->check_type(m, ctx, infer_only);
-    }
-    optional<expr> expand(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand(m, ctx); }
-    optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand1(m, ctx); }
-    unsigned trust_level() const { return m_ptr->trust_level(); }
-    bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
-    bool operator!=(macro_definition const & other) const { return !operator==(other); }
-    bool operator<(macro_definition const & other) const;
-    void display(std::ostream & out) const { return m_ptr->display(out); }
-    unsigned hash() const { return m_ptr->hash(); }
-    void write(serializer & s) const { return m_ptr->write(s); }
-    macro_definition_cell const * raw() const { return m_ptr; }
-
-    friend bool is_eqp(macro_definition const & d1, macro_definition const & d2) {
-        return d1.m_ptr == d2.m_ptr;
-    }
-};
-
-/** \brief Macro attachments */
-class expr_macro : public expr_composite {
-    macro_definition m_definition;
-    unsigned         m_num_args;
-    friend class expr_cell;
-    friend expr copy(expr const & a);
-    friend expr update_macro(expr const & e, unsigned num, expr const * args);
-    void dealloc(buffer<expr_cell*> & todelete);
-    expr * get_args_ptr() {
-        return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
-    }
-    expr const * get_args_ptr() const {
-        return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
-    }
-    friend struct cache_expr_insert_fn;
-    expr_macro(expr_macro const & src, expr const * new_args); // for hash_consing
-public:
-    expr_macro(macro_definition const & v, unsigned num, expr const * args);
-    ~expr_macro();
-
-    macro_definition const & get_def() const { return m_definition; }
-    expr const * get_args() const { return get_args_ptr(); }
-    expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
-    unsigned get_num_args() const { return m_num_args; }
-};
 
 // =======================================
 // Testers
 inline bool is_bvar(expr_ptr e)        { return e->kind() == expr_kind::BVar; }
-inline bool is_fvar(expr_ptr e)       { return e->kind() == expr_kind::FVar; }
+inline bool is_fvar(expr_ptr e)        { return e->kind() == expr_kind::FVar; }
 inline bool is_constant(expr_ptr e)    { return e->kind() == expr_kind::Constant; }
 inline bool is_metavar(expr_ptr e)     { return e->kind() == expr_kind::Meta; }
-inline bool is_macro(expr_ptr e)       { return e->kind() == expr_kind::Macro; }
 inline bool is_app(expr_ptr e)         { return e->kind() == expr_kind::App; }
 inline bool is_lambda(expr_ptr e)      { return e->kind() == expr_kind::Lambda; }
 inline bool is_pi(expr_ptr e)          { return e->kind() == expr_kind::Pi; }
@@ -547,6 +468,7 @@ inline unsigned get_loose_bvar_range(expr const & e) {
     switch (e.kind()) {
     case expr_kind::BVar:                           return bvar_idx(e) + 1;
     case expr_kind::Constant: case expr_kind::Sort: return 0;
+    case expr_kind::Quote:                          return 0;
     default:                                        return static_cast<expr_composite*>(e.raw())->m_loose_bvar_range;
     }
 }
@@ -596,7 +518,6 @@ expr update_local(expr const & e, expr const & new_type, binder_info const & bi)
 expr update_local(expr const & e, binder_info const & bi);
 expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
-expr update_macro(expr const & e, unsigned num, expr const * args);
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
 // =======================================
 
@@ -649,15 +570,117 @@ void finalize_expr();
    The following API is to support legacy code
    -------------------------------- */
 
+// TODO(Leo): delete
+class expr_quote : public expr_cell {
+    bool m_reflected;
+    expr m_value;
+    friend class expr_cell;
+    void dealloc(buffer<expr_cell*> & todelete);
+public:
+    expr_quote(bool r, expr const & v);
+    ~expr_quote() {}
+    bool is_reflected() const { return m_reflected; }
+    expr const & get_value() const { return m_value; }
+};
+
+/** \brief Abstract class for macro_definitions */
+class macro_definition_cell {
+protected:
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
+    /**
+       \brief Auxiliary method used for implementing a total order on macro
+       attachments. It is invoked by operator<, and it is only invoked when
+       <tt>get_name() == other.get_name()</tt>
+    */
+    virtual bool lt(macro_definition_cell const &) const;
+public:
+    macro_definition_cell():m_rc(0) {}
+    virtual ~macro_definition_cell() {}
+    virtual name get_name() const = 0;
+    virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const = 0;
+    virtual optional<expr> expand(expr const & m, abstract_type_context & ctx) const = 0;
+    virtual optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return expand(m, ctx); }
+    virtual unsigned trust_level() const;
+    virtual bool operator==(macro_definition_cell const & other) const;
+    virtual void display(std::ostream & out) const;
+    virtual unsigned hash() const;
+    virtual void write(serializer & s) const = 0;
+    typedef std::function<expr(deserializer&, unsigned, expr const *)> reader;
+};
+
+/** \brief Smart pointer for macro definitions */
+class macro_definition {
+public:
+    macro_definition_cell * m_ptr;
+public:
+    explicit macro_definition(macro_definition_cell * ptr);
+    macro_definition(macro_definition const & s);
+    macro_definition(macro_definition && s);
+    ~macro_definition();
+
+    macro_definition & operator=(macro_definition const & s);
+    macro_definition & operator=(macro_definition && s);
+
+    name get_name() const { return m_ptr->get_name(); }
+    expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
+        return m_ptr->check_type(m, ctx, infer_only);
+    }
+    optional<expr> expand(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand(m, ctx); }
+    optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand1(m, ctx); }
+    unsigned trust_level() const { return m_ptr->trust_level(); }
+    bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
+    bool operator!=(macro_definition const & other) const { return !operator==(other); }
+    bool operator<(macro_definition const & other) const;
+    void display(std::ostream & out) const { return m_ptr->display(out); }
+    unsigned hash() const { return m_ptr->hash(); }
+    void write(serializer & s) const { return m_ptr->write(s); }
+    macro_definition_cell const * raw() const { return m_ptr; }
+
+    friend bool is_eqp(macro_definition const & d1, macro_definition const & d2) {
+        return d1.m_ptr == d2.m_ptr;
+    }
+};
+
+/** \brief Macro attachments */
+class expr_macro : public expr_composite {
+    macro_definition m_definition;
+    unsigned         m_num_args;
+    friend class expr_cell;
+    friend expr copy(expr const & a);
+    friend expr update_macro(expr const & e, unsigned num, expr const * args);
+    void dealloc(buffer<expr_cell*> & todelete);
+    expr * get_args_ptr() {
+        return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
+    }
+    expr const * get_args_ptr() const {
+        return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
+    }
+    friend struct cache_expr_insert_fn;
+    expr_macro(expr_macro const & src, expr const * new_args); // for hash_consing
+public:
+    expr_macro(macro_definition const & v, unsigned num, expr const * args);
+    ~expr_macro();
+
+    macro_definition const & get_def() const { return m_definition; }
+    expr const * get_args() const { return get_args_ptr(); }
+    expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
+    unsigned get_num_args() const { return m_num_args; }
+};
+
 inline bool is_var(expr_ptr e) { return is_bvar(e); }
 inline bool is_local(expr_ptr e) { return is_fvar(e); }
 inline bool is_mlocal(expr_ptr e) { return is_metavar(e) || is_local(e); }
+inline bool is_quote(expr_ptr e)       { return e->kind() == expr_kind::Quote; }
+inline bool is_macro(expr_ptr e)       { return e->kind() == expr_kind::Macro; }
 inline unsigned var_idx(expr_ptr e) { return bvar_idx(e); }
 inline bool is_var(expr_ptr e, unsigned i) { return is_bvar(e, i); }
 inline expr_bvar *        to_var(expr_ptr e)        { return to_bvar(e); }
 inline expr_mlocal *      to_mlocal(expr_ptr e)     { lean_assert(is_mlocal(e));      return static_cast<expr_mlocal*>(e); }
 inline expr_fvar *      to_local(expr_ptr e)     { return to_fvar(e); }
 inline expr_macro *       to_macro(expr_ptr e)      { lean_assert(is_macro(e));       return static_cast<expr_macro*>(e); }
+inline expr_quote *       to_quote(expr_ptr e)      { lean_assert(is_quote(e));       return static_cast<expr_quote*>(e); }
+
 inline name const &   mlocal_name(expr_ptr e)  { return to_mlocal(e)->get_name(); }
 inline expr const &   mlocal_type(expr_ptr e)  { return to_mlocal(e)->get_type(); }
 inline name const &   mlocal_pp_name(expr_ptr e) { return to_mlocal(e)->get_pp_name(); }
@@ -669,6 +692,7 @@ inline unsigned       macro_num_args(expr_ptr e)        { return to_macro(e)->ge
 inline expr mk_var(unsigned idx) { return mk_bvar(idx); }
 inline expr Var(unsigned idx) { return mk_bvar(idx); }
 expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr);
+expr mk_quote(bool reflected, expr const & val);
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
 inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, binder_info()); }
 inline expr mk_local(name const & n, expr const & t, binder_info const & bi) {
@@ -678,4 +702,9 @@ inline expr Local(name const & n, expr const & t, binder_info const & bi = binde
     return mk_local(n, t, bi);
 }
 inline bool has_local(expr const & e) { return has_fvar(e); }
+expr update_macro(expr const & e, unsigned num, expr const * args);
+
+inline bool quote_is_reflected(expr const & e) { return to_quote(e)->is_reflected(); }
+inline expr const & quote_value(expr const & e) { return to_quote(e)->get_value(); }
+
 }
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 9fbc35b877..1d6bb6cf4f 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -108,6 +108,8 @@ class expr_eq_fn {
                 (!CompareBinderInfo || let_name(a) == let_name(b));
         case expr_kind::Sort:
             return sort_level(a) == sort_level(b);
+
+
         case expr_kind::Macro:
             check_system();
             if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
@@ -117,6 +119,10 @@ class expr_eq_fn {
                     return false;
             }
             return true;
+        case expr_kind::Quote:
+            /* Hack: we do *not* compare m_value's because quoted expressions may contain
+               relevant position information that is ignored by the equality predicate for expressions. */
+            return a.raw() == b.raw();
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index e0f6b17883..47f3d24b86 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -95,14 +95,6 @@ class for_each_fn {
             case expr_kind::Meta:
                 todo.emplace_back(mlocal_type(e), offset);
                 goto begin_loop;
-            case expr_kind::Macro: {
-                unsigned i = macro_num_args(e);
-                while (i > 0) {
-                    --i;
-                    todo.emplace_back(macro_arg(e, i), offset);
-                }
-                goto begin_loop;
-            }
             case expr_kind::App:
                 todo.emplace_back(app_arg(e), offset);
                 todo.emplace_back(app_fn(e), offset);
@@ -116,6 +108,16 @@ class for_each_fn {
                 todo.emplace_back(let_value(e), offset);
                 todo.emplace_back(let_type(e), offset);
                 goto begin_loop;
+            case expr_kind::Macro: {
+                unsigned i = macro_num_args(e);
+                while (i > 0) {
+                    --i;
+                    todo.emplace_back(macro_arg(e, i), offset);
+                }
+                goto begin_loop;
+            }
+            case expr_kind::Quote:
+                goto begin_loop;
             }
         }
     }
diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp
index f480017e2d..1fd7b0ca16 100644
--- a/src/kernel/old_type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -25,6 +25,10 @@ namespace lean {
 static name * g_kernel_fresh = nullptr;
 static expr * g_dont_care    = nullptr;
 
+[[noreturn]] static void throw_found_quote(environment const & env) {
+    throw kernel_exception(env, "unexpected quoted expression");
+}
+
 optional<expr> old_type_checker::expand_macro(expr const & m) {
     lean_assert(is_macro(m));
     return macro_def(m).expand(m, *this);
@@ -227,6 +231,8 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
     case expr_kind::Pi:        r = infer_pi(e, infer_only);             break;
     case expr_kind::App:       r = infer_app(e, infer_only);            break;
     case expr_kind::Let:       r = infer_let(e, infer_only);            break;
+
+    case expr_kind::Quote: throw_found_quote(m_env);
     }
 
     if (m_memoize)
@@ -282,6 +288,7 @@ expr old_type_checker::whnf_core(expr const & e) {
         return e;
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
         break;
+    case expr_kind::Quote: throw_found_quote(m_env);
     }
 
     // check cache
@@ -331,6 +338,7 @@ expr old_type_checker::whnf_core(expr const & e) {
     case expr_kind::Let:
         r = whnf_core(instantiate(let_body(e), let_value(e)));
         break;
+    case expr_kind::Quote: throw_found_quote(m_env);
     }
 
     if (m_memoize)
@@ -385,6 +393,7 @@ expr old_type_checker::whnf(expr const & e) {
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
     case expr_kind::Constant: case expr_kind::Let:
         break;
+    case expr_kind::Quote: throw_found_quote(m_env);
     }
 
     // check cache
@@ -479,6 +488,7 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
         case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
+        case expr_kind::Quote: throw_found_quote(m_env);
         }
     }
     return l_undef; // This is not an "easy case"
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index a256f8cfc4..148219afc0 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -111,7 +111,10 @@ class replace_rec_fn {
                 for (unsigned i = 0; i < nargs; i++)
                     new_args.push_back(apply(macro_arg(e, i), offset));
                 return save_result(e, offset, update_macro(e, new_args.size(), new_args.data()), shared);
-            }}
+            }
+            case expr_kind::Quote:
+                return save_result(e, offset, e, shared);
+            }
             lean_unreachable();
         }
     }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 9772d07be3..4f1c8513cc 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -227,11 +227,20 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
         r = mk_sort(mk_succ(sort_level(e)));
         break;
     case expr_kind::Constant:  r = infer_constant(e, infer_only);       break;
-    case expr_kind::Macro:     r = infer_macro(e, infer_only);          break;
     case expr_kind::Lambda:    r = infer_lambda(e, infer_only);         break;
     case expr_kind::Pi:        r = infer_pi(e, infer_only);             break;
     case expr_kind::App:       r = infer_app(e, infer_only);            break;
     case expr_kind::Let:       r = infer_let(e, infer_only);            break;
+
+    case expr_kind::Macro:     r = infer_macro(e, infer_only);          break;
+    case expr_kind::Quote:
+        if (quote_is_reflected(e)) {
+            expr type = infer_type_core(quote_value(e), true);
+            level u   = sort_level(ensure_sort_core(infer_type_core(type, true), e));
+            return mk_app(mk_constant(name("reflected"), {u}), type, quote_value(e));
+        } else {
+            return mk_constant(name("pexpr"));
+        }
     }
 
     if (m_memoize)
@@ -299,6 +308,9 @@ expr type_checker::whnf_core(expr const & e) {
         return whnf_fvar(e);
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
         break;
+
+    case expr_kind::Quote:
+        return e;
     }
 
     // check cache
@@ -314,6 +326,10 @@ expr type_checker::whnf_core(expr const & e) {
     case expr_kind::BVar:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
         lean_unreachable(); // LCOV_EXCL_LINE
+
+    case expr_kind::Quote:
+        lean_unreachable();
+
     case expr_kind::Macro:
         if (auto m = expand_macro(e))
             r = whnf_core(*m);
@@ -404,6 +420,9 @@ expr type_checker::whnf(expr const & e) {
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
     case expr_kind::Constant: case expr_kind::Let:
         break;
+
+    case expr_kind::Quote:
+        return e;
     }
 
     // check cache
@@ -499,6 +518,9 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
         case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
+
+        case expr_kind::Quote:
+            return to_lbool(t.raw() == s.raw());
         }
     }
     return l_undef; // This is not an "easy case"
diff --git a/src/library/check.cpp b/src/library/check.cpp
index 2a102a1b67..eea8d19642 100644
--- a/src/library/check.cpp
+++ b/src/library/check.cpp
@@ -116,8 +116,6 @@ struct check_fn {
             return visit_constant(e);
         case expr_kind::BVar:
             lean_unreachable();  // LCOV_EXCL_LINE
-        case expr_kind::Macro:
-            return visit_macro(e);
         case expr_kind::Lambda:
             return visit_lambda(e);
         case expr_kind::Pi:
@@ -126,6 +124,10 @@ struct check_fn {
             return visit_app(e);
         case expr_kind::Let:
             return visit_let(e);
+        case expr_kind::Macro:
+            return visit_macro(e);
+        case expr_kind::Quote:
+            break; /* do nothing */
         }
     }
 
diff --git a/src/library/compiler/comp_irrelevant.cpp b/src/library/compiler/comp_irrelevant.cpp
index dfeb3bb6ad..b7327e787b 100644
--- a/src/library/compiler/comp_irrelevant.cpp
+++ b/src/library/compiler/comp_irrelevant.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/annotation.h"
-#include "library/quote.h"
 #include "library/compiler/util.h"
 #include "library/compiler/compiler_step_visitor.h"
 
diff --git a/src/library/compiler/compiler_step_visitor.cpp b/src/library/compiler/compiler_step_visitor.cpp
index 9d63cc6ef4..4dadc854e6 100644
--- a/src/library/compiler/compiler_step_visitor.cpp
+++ b/src/library/compiler/compiler_step_visitor.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
-#include "library/quote.h"
 #include "library/compiler/compiler_step_visitor.h"
 #include "library/compiler/comp_irrelevant.h"
 
diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index 206852ef02..1c378e28f1 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -56,7 +56,8 @@ class cse_fn : public compiler_step_visitor {
             case expr_kind::Macro:    visit_macro(e); break;
             case expr_kind::App:      visit_app(e); break;
             case expr_kind::Let:      visit_let(e); break;
-            default: break;
+            case expr_kind::Quote:
+                break;
             }
         }
     public:
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index b9c025f658..7bd51b60fd 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -12,7 +12,6 @@ Author: Leonardo de Moura
 #include "library/normalize.h"
 #include "library/inverse.h"
 #include "library/aux_recursors.h"
-#include "library/quote.h"
 #include "library/inductive_compiler/ginductive.h"
 #include "library/compiler/util.h"
 #include "library/compiler/nat_value.h"
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index dbaa205408..d7a99e357a 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "library/aux_recursors.h"
 #include "library/user_recursors.h"
 #include "library/util.h"
-#include "library/quote.h"
 #include "library/noncomputable.h"
 #include "library/context_cache.h"
 #include "library/module.h"
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 68433a65a7..e03e645c57 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -289,6 +289,10 @@ class vm_compiler_fn {
         }
     }
 
+    void compile_quote(expr const & e) {
+        emit(mk_expr_instr(quote_value(e)));
+    }
+
     void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         switch (e.kind()) {
         case expr_kind::BVar:     lean_unreachable();
@@ -301,6 +305,7 @@ class vm_compiler_fn {
         case expr_kind::FVar:     compile_local(e, m);       break;
         case expr_kind::App:      compile_app(e, bpz, m);    break;
         case expr_kind::Let:      compile_let(e, bpz, m);    break;
+        case expr_kind::Quote:    compile_quote(e); break;
         }
     }
 
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index 5635a88e0b..0318ade7d8 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -21,6 +21,7 @@ expr copy(expr const & a) {
     case expr_kind::Meta:     return mk_metavar(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a));
     case expr_kind::FVar:     return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
     case expr_kind::Let:      return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
+    case expr_kind::Quote:    return mk_quote(quote_is_reflected(a), quote_value(a));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 3ca6f135cd..1dd0bef907 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -118,11 +118,6 @@ struct structural_rec_fn {
             case expr_kind::FVar: case expr_kind::Constant:
             case expr_kind::Sort:
                 return true;
-            case expr_kind::Macro:
-                for (unsigned i = 0; i < macro_num_args(e); i++)
-                    if (!check_rhs(macro_arg(e, i)))
-                        return false;
-                return true;
             case expr_kind::App: {
                 buffer<expr> args;
                 expr const & fn = get_app_args(e, args);
@@ -171,6 +166,15 @@ struct structural_rec_fn {
                     type_context_old::tmp_locals locals(m_ctx);
                     return check_rhs(instantiate(binding_body(e), locals.push_local_from_binding(e)));
                 }
+
+
+            case expr_kind::Macro:
+                for (unsigned i = 0; i < macro_num_args(e); i++)
+                    if (!check_rhs(macro_arg(e, i)))
+                        return false;
+                return true;
+            case expr_kind::Quote:
+                return true;
             }
             lean_unreachable();
         }
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index c292ff8e1e..8318a6ba8a 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -69,6 +69,8 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
                 return is_lt(macro_arg(a, i), macro_arg(b, i), use_hash, lctx);
         }
         return false;
+    case expr_kind::Quote:
+        return quote_value(a) < quote_value(b);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -179,6 +181,8 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
                 return false;
         }
         return false;
+    case expr_kind::Quote:
+        return quote_value(a) < quote_value(b);
     }
     lean_unreachable();
 }
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index ead1c0564c..6775b1ea1c 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -533,6 +533,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Sort:
         case expr_kind::FVar:
         case expr_kind::Macro:
+        case expr_kind::Quote:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
@@ -587,6 +588,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Sort:
         case expr_kind::FVar:
         case expr_kind::Macro:
+        case expr_kind::Quote:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 7b8aec3585..7960db72d0 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -84,13 +84,6 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
                 case expr_kind::Sort:
                     s << sort_level(a);
                     break;
-                case expr_kind::Macro:
-                    s << macro_num_args(a);
-                    for (unsigned i = 0; i < macro_num_args(a); i++) {
-                        write_core(macro_arg(a, i));
-                    }
-                    macro_def(a).write(s);
-                    break;
                 case expr_kind::App:
                     write_core(app_fn(a)); write_core(app_arg(a));
                     break;
@@ -112,6 +105,18 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
                     lean_assert(!mlocal_pp_name(a).is_anonymous());
                     s << mlocal_name(a) << mlocal_pp_name(a) << local_info(a); write_core(mlocal_type(a));
                     break;
+
+                case expr_kind::Macro:
+                    s << macro_num_args(a);
+                    for (unsigned i = 0; i < macro_num_args(a); i++) {
+                        write_core(macro_arg(a, i));
+                    }
+                    macro_def(a).write(s);
+                    break;
+                case expr_kind::Quote:
+                    s << quote_is_reflected(a);
+                    write_core(quote_value(a));
+                    break;
                 }
             });
     }
@@ -146,14 +151,6 @@ public:
                 }
                 case expr_kind::Sort:
                     return mk_sort(read_level(d));
-                case expr_kind::Macro: {
-                    unsigned n = d.read_unsigned();
-                    buffer<expr> args;
-                    for (unsigned i = 0; i < n; i++) {
-                        args.push_back(read());
-                    }
-                    return read_macro_definition(d, args.size(), args.data());
-                }
                 case expr_kind::App: {
                     expr f = read();
                     return mk_app(f, read());
@@ -176,7 +173,22 @@ public:
                     name pp_n      = read_name(d);
                     binder_info bi = read_binder_info(d);
                     return mk_local(n, pp_n, read(), bi);
-                }}
+                }
+
+                case expr_kind::Macro: {
+                    unsigned n = d.read_unsigned();
+                    buffer<expr> args;
+                    for (unsigned i = 0; i < n; i++) {
+                        args.push_back(read());
+                    }
+                    return read_macro_definition(d, args.size(), args.data());
+                }
+                case expr_kind::Quote: {
+                    bool r = d.read_bool();
+                    expr v = read();
+                    return mk_quote(r, v);
+                }
+                }
                 throw corrupted_stream_exception(); // LCOV_EXCL_LINE
             });
     }
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index ab49a2a264..dd393935cf 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -83,10 +83,6 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
             lean_assert(!restricted);
             visit(mlocal_type(e));
             break;
-        case expr_kind::Macro:
-            for (unsigned i = 0; i < macro_num_args(e); i++)
-                visit(macro_arg(e, i));
-            break;
         case expr_kind::App:
             visit(app_fn(e));
             visit(app_arg(e));
@@ -101,6 +97,14 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
             visit(let_value(e));
             visit(let_body(e));
             break;
+
+        case expr_kind::Macro:
+            for (unsigned i = 0; i < macro_num_args(e); i++)
+                visit(macro_arg(e, i));
+            break;
+        case expr_kind::Quote:
+            break; // do nothing
+
         }
     };
     visit(e);
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 6c57deb400..7faffa4c0b 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -90,7 +90,11 @@ struct max_sharing_fn::imp {
                 new_args.push_back(macro_arg(a, i));
             res = update_macro(a, new_args.size(), new_args.data());
             break;
-        }}
+        }
+        case expr_kind::Quote:
+            res = a;
+            break;
+        }
         m_expr_cache.insert(res);
         return res;
     }
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 4fef23da17..b512896238 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -199,6 +199,7 @@ struct get_noncomputable_reason_fn {
         case expr_kind::Lambda:    visit_binding(e);  return;
         case expr_kind::Pi:        visit_binding(e);  return;
         case expr_kind::Let:       visit_let(e);      return;
+        case expr_kind::Quote:     return;
         }
     }
 
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index a05cdbda94..134bcf629c 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -117,7 +117,7 @@ class normalize_fn {
         e = m_ctx.whnf(e);
         switch (e.kind()) {
         case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
-        case expr_kind::Meta: case expr_kind::FVar: case expr_kind::Macro:
+        case expr_kind::Meta: case expr_kind::FVar:
             return e;
         case expr_kind::Lambda: {
             e = normalize_binding(e);
@@ -133,6 +133,10 @@ class normalize_fn {
         case expr_kind::Let:
             // whnf unfolds let-exprs
             lean_unreachable();
+
+        case expr_kind::Macro:
+        case expr_kind::Quote:
+            return e;
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp
index b501410288..57e9781f5f 100644
--- a/src/library/pos_info_provider.cpp
+++ b/src/library/pos_info_provider.cpp
@@ -164,7 +164,10 @@ class replace_rec_fn2 {
                 for (unsigned i = 0; i < nargs; i++)
                     new_args.push_back(apply(macro_arg(e, i), offset));
                 return save_result(e, offset, copy_pos(e, update_macro(e, new_args.size(), new_args.data())), shared);
-            }}
+            }
+            case expr_kind::Quote:
+                return save_result(e, offset, e, shared);
+            }
             lean_unreachable();
         }
     }
diff --git a/src/library/print.cpp b/src/library/print.cpp
index b78b7c5179..09e50b8453 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -251,6 +251,10 @@ struct print_expr_fn {
         case expr_kind::Macro:
             print_macro(a);
             break;
+        case expr_kind::Quote:
+            out() << "quote " << quote_is_reflected(a) << " ";
+            print(quote_value(a));
+            break;
         }
     }
 
diff --git a/src/library/quote.cpp b/src/library/quote.cpp
index 1c7f1d8ebe..84e0b2d7cf 100644
--- a/src/library/quote.cpp
+++ b/src/library/quote.cpp
@@ -22,85 +22,34 @@ static std::string * g_expr_quote_opcode  = nullptr;
 static expr * g_expr                = nullptr;
 static expr * g_pexpr               = nullptr;
 static name * g_expr_quote_pre      = nullptr;
-static name * g_expr_quote_macro    = nullptr;
-
-/** \brief A compact way of encoding quoted expressions inside Lean expressions. Used for values of type
-    `reflected e` and `pexpr`. */
-class expr_quote_macro : public macro_definition_cell {
-    expr m_value;
-    bool m_reflected;
-public:
-    expr_quote_macro(expr const & v, bool reflected):m_value(v), m_reflected(reflected) {}
-    virtual bool lt(macro_definition_cell const & d) const override {
-        return m_value < static_cast<expr_quote_macro const &>(d).m_value;
-    }
-    virtual name get_name() const override { return *g_expr_quote_macro; }
-    virtual expr check_type(expr const &, abstract_type_context & ctx, bool infer_only) const override {
-        if (m_reflected) {
-            expr ty = ctx.check(m_value, infer_only);
-            return mk_app(mk_constant(get_reflected_name(), {get_level(ctx, ty)}), ty, m_value);
-        } else {
-            return *g_pexpr;
-        }
-    }
-    virtual optional<expr> expand(expr const &, abstract_type_context &) const override {
-        return optional<expr>();
-    }
-    virtual unsigned trust_level() const override { return 0; }
-    virtual bool operator==(macro_definition_cell const & other) const override {
-        /* Hack: we do *not* compare m_value's because quoted expressions may contain
-           relevant position information that is ignored by the equality predicate for expressions.
-        */
-        return this == &other;
-    }
-    char const * prefix() const {
-        return m_reflected ? "`(" : "``(";
-    }
-    virtual void display(std::ostream & out) const override {
-        out << prefix() << m_value << ")";
-    }
-    virtual unsigned hash() const override { return m_value.hash(); }
-    virtual void write(serializer & s) const override { s << *g_expr_quote_opcode << m_value << m_reflected; }
-    expr const & get_value() const { return m_value; }
-    bool const & is_reflected() const { return m_reflected; }
-};
 
 expr mk_elaborated_expr_quote(expr const & e) {
-    return mk_macro(macro_definition(new expr_quote_macro(e, /* reflected */ true)));
+    return mk_quote(true, e);
 }
+
 expr mk_unelaborated_expr_quote(expr const & e) {
     // We use a transparent annotation instead of the opaque macro above so that the quoted term is accessible to
     // collect_locals etc.
     return mk_annotation(*g_expr_quote_pre, e);
 }
+
 expr mk_pexpr_quote(expr const & e) {
-    return mk_macro(macro_definition(new expr_quote_macro(e, /* reflected */ false)));
+    return mk_quote(false, e);
 }
 
 bool is_expr_quote(expr const & e) {
-    if (is_annotation(e, *g_expr_quote_pre)) {
-        return true;
-    }
-    if (is_macro(e)) {
-        if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
-            return m->is_reflected();
-        }
-    }
-    return false;
+    return
+        (is_annotation(e, *g_expr_quote_pre)) ||
+        (is_quote(e) && quote_is_reflected(e));
 }
 bool is_pexpr_quote(expr const & e) {
-    if (is_macro(e)) {
-        if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
-            return !m->is_reflected();
-        }
-    }
-    return false;
+    return is_quote(e) && !quote_is_reflected(e);
 }
 
 expr const & get_expr_quote_value(expr const & e) {
     lean_assert(is_expr_quote(e));
-    if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
-        return m->get_value();
+    if (is_quote(e)) {
+        return quote_value(e);
     } else {
         return get_annotation_arg(e);
     }
@@ -108,7 +57,7 @@ expr const & get_expr_quote_value(expr const & e) {
 
 expr const & get_pexpr_quote_value(expr const & e) {
     lean_assert(is_pexpr_quote(e));
-    return static_cast<expr_quote_macro const *>(macro_def(e).raw())->get_value();
+    return quote_value(e);
 }
 
 static name * g_antiquote = nullptr;
@@ -152,8 +101,6 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
 void initialize_quote() {
     g_quote_fresh         = new name("_quote_fresh");
     register_name_generator_prefix(*g_quote_fresh);
-    g_expr_quote_macro    = new name("expr_quote_macro");
-    g_expr_quote_opcode   = new std::string("Quote");
     g_expr           = new expr(mk_app(Const(get_expr_name()), mk_bool_tt()));
     g_pexpr          = new expr(mk_constant(get_pexpr_name()));
 
@@ -161,21 +108,11 @@ void initialize_quote() {
     g_expr_quote_pre = new name("expr_quote_pre");
     register_annotation(*g_antiquote);
     register_annotation(*g_expr_quote_pre);
-
-    register_macro_deserializer(*g_expr_quote_opcode,
-                                [](deserializer & d, unsigned num, expr const *) {
-                                    if (num != 0)
-                                        throw corrupted_stream_exception();
-                                    expr e; bool reflected;
-                                    d >> e >> reflected;
-                                    return mk_macro(macro_definition(new expr_quote_macro(e, reflected)));
-                                });
 }
 
 void finalize_quote() {
     delete g_quote_fresh;
     delete g_expr_quote_pre;
-    delete g_expr_quote_macro;
     delete g_expr_quote_opcode;
     delete g_expr;
     delete g_pexpr;
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index df1d48f4d5..e9758b0e7f 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 namespace lean {
 expr replace_visitor::visit_sort(expr const & e) { lean_assert(is_sort(e)); return e; }
 expr replace_visitor::visit_var(expr const & e) { lean_assert(is_var(e)); return e; }
+expr replace_visitor::visit_quote(expr const & e) { lean_assert(is_quote(e)); return e; }
 expr replace_visitor::visit_constant(expr const & e) { lean_assert(is_constant(e)); return e; }
 expr replace_visitor::visit_mlocal(expr const & e) {
     lean_assert(is_mlocal(e));
@@ -67,7 +68,6 @@ expr replace_visitor::visit(expr const & e) {
 
     switch (e.kind()) {
     case expr_kind::Sort:      return save_result(e, visit_sort(e), shared);
-    case expr_kind::Macro:     return save_result(e, visit_macro(e), shared);
     case expr_kind::Constant:  return save_result(e, visit_constant(e), shared);
     case expr_kind::BVar:      return save_result(e, visit_var(e), shared);
     case expr_kind::Meta:      return save_result(e, visit_meta(e), shared);
@@ -76,8 +76,10 @@ expr replace_visitor::visit(expr const & e) {
     case expr_kind::Lambda:    return save_result(e, visit_lambda(e), shared);
     case expr_kind::Pi:        return save_result(e, visit_pi(e), shared);
     case expr_kind::Let:       return save_result(e, visit_let(e), shared);
-    }
 
+    case expr_kind::Macro:     return save_result(e, visit_macro(e), shared);
+    case expr_kind::Quote:     return save_result(e, visit_quote(e), shared);
+    }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 }
diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h
index 6edaa7aec8..de131ca312 100644
--- a/src/library/replace_visitor.h
+++ b/src/library/replace_visitor.h
@@ -19,7 +19,6 @@ protected:
     cache   m_cache;
     expr save_result(expr const & e, expr && r, bool shared);
     virtual expr visit_sort(expr const &);
-    virtual expr visit_macro(expr const &);
     virtual expr visit_constant(expr const &);
     virtual expr visit_var(expr const &);
     virtual expr visit_mlocal(expr const &);
@@ -31,6 +30,9 @@ protected:
     virtual expr visit_pi(expr const &);
     virtual expr visit_let(expr const & e);
     virtual expr visit(expr const &);
+
+    virtual expr visit_macro(expr const &);
+    virtual expr visit_quote(expr const &);
 public:
     expr operator()(expr const & e) { return visit(e); }
     void clear() { m_cache.clear(); }
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index b248bf4766..eb967bad02 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -264,9 +264,6 @@ expr dsimplify_core_fn::visit(expr const & e) {
         case expr_kind::Meta:
             new_e = visit_meta(curr_e);
             break;
-        case expr_kind::Macro:
-            new_e = visit_macro(curr_e);
-            break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
             new_e = visit_binding(curr_e);
@@ -277,6 +274,14 @@ expr dsimplify_core_fn::visit(expr const & e) {
         case expr_kind::Let:
             new_e = visit_let(curr_e);
             break;
+
+
+        case expr_kind::Macro:
+            new_e = visit_macro(curr_e);
+            break;
+        case expr_kind::Quote:
+            new_e = curr_e;
+            break;
         }
 
         if (auto p2 = post(new_e)) {
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index c6a93a2462..94760cf36e 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -665,6 +665,8 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
                 return false;
         }
         return true;
+    case expr_kind::Quote:
+        return lhs == rhs;
     }
     lean_unreachable();
 }
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 373dceb3e2..f098583abe 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -653,9 +653,6 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
             new_result = curr_result;
             new_result.update(m_ctx.instantiate_mvars(new_result.get_new()));
             break;
-        case expr_kind::Macro:
-            new_result = join(curr_result, visit_macro(curr_result.get_new()));
-            break;
         case expr_kind::BVar:
             lean_unreachable();
         case expr_kind::Lambda:
@@ -670,6 +667,13 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         case expr_kind::Let:
             new_result = join(curr_result, visit_let(curr_result.get_new()));
             break;
+
+        case expr_kind::Macro:
+            new_result = join(curr_result, visit_macro(curr_result.get_new()));
+            break;
+        case expr_kind::Quote:
+            new_result = curr_result;
+            break;
         }
 
         if (m_cfg.m_constructor_eq && simplify_constructor_eq_constructor(new_result)) {
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 20220017df..0ea1aa73c6 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -820,14 +820,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
             }
         }
         return e;
-    case expr_kind::Macro:
-        if (auto m = expand_macro(e)) {
-            check_system("whnf");
-            e = *m;
-            continue;
-        } else {
-            return e;
-        }
     case expr_kind::Let:
         check_system("whnf");
         if (use_zeta()) {
@@ -882,7 +874,19 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
             e = mk_rev_app(f, args.size(), args.data());
             continue;
         }
-    }}}
+    }
+
+    case expr_kind::Macro:
+        if (auto m = expand_macro(e)) {
+            check_system("whnf");
+            e = *m;
+            continue;
+        } else {
+            return e;
+        }
+    case expr_kind::Quote:
+        return e;
+    }}
 }
 
 expr type_context_old::whnf(expr const & e) {
@@ -1011,9 +1015,6 @@ expr type_context_old::infer_core(expr const & e) {
     case expr_kind::Constant:
         r = infer_constant(e);
         break;
-    case expr_kind::Macro:
-        r = infer_macro(e);
-        break;
     case expr_kind::Lambda:
         r = infer_lambda(e);
         break;
@@ -1026,6 +1027,17 @@ expr type_context_old::infer_core(expr const & e) {
     case expr_kind::Let:
         r = infer_let(e);
         break;
+
+    case expr_kind::Macro:
+        r = infer_macro(e);
+        break;
+    case expr_kind::Quote:
+        if (quote_is_reflected(e)) {
+            expr type = infer_core(quote_value(e));
+            return mk_app(mk_constant(get_reflected_name(), {get_level(type)}), type, quote_value(e));
+        } else {
+            return mk_constant(get_pexpr_name());
+        }
     }
 
     if ((!in_tmp_mode() || (!has_expr_metavar(e) && !has_expr_metavar(r))) &&
@@ -2704,10 +2716,16 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
             return to_lbool(is_def_eq(sort_level(e1), sort_level(e2)));
         case expr_kind::Meta:     case expr_kind::BVar:
         case expr_kind::FVar:     case expr_kind::App:
-        case expr_kind::Constant: case expr_kind::Macro:
+        case expr_kind::Constant:
         case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
+
+        case expr_kind::Macro:
+            // We do not handle these cases in this method.
+            break;
+        case expr_kind::Quote:
+            return to_lbool(quote_is_reflected(e1) == quote_is_reflected(e2) && quote_value(e1) == quote_value(e2));
         }
     }
     return l_undef; // This is not an "easy case"
@@ -3326,8 +3344,6 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
             return l_false;
         case expr_kind::Let:
             return l_undef;
-        case expr_kind::Macro:
-            return l_undef;
         case expr_kind::Constant:
             if (auto r = constant_is_class(*it)) {
                 result = *r;
@@ -3357,6 +3373,10 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
         case expr_kind::Pi:
             it = &binding_body(*it);
             break;
+        case expr_kind::Macro:
+            return l_undef;
+        case expr_kind::Quote:
+            return l_false;
         }
     }
 }
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 6b478bec5b..471ef0910d 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -196,13 +196,19 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
         data.push_back(to_obj(let_value(e)));
         data.push_back(to_obj(let_body(e)));
         break;
-    case expr_kind::Macro:
+
+    case expr_kind::Macro: {
         data.push_back(to_obj(macro_def(e)));
         buffer<expr> args;
         args.append(macro_num_args(e), macro_args(e));
         data.push_back(to_obj(args));
         break;
     }
+    case expr_kind::Quote:
+        data.push_back(to_obj(quote_is_reflected(e)));
+        data.push_back(to_obj(quote_value(e)));
+        break;
+    }
     return static_cast<unsigned>(e.kind());
 }