diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 398d4e1f89..dbd7f27354 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -63,9 +63,9 @@ class constant_val : public object_ref {
 public:
     constant_val(name const & n, names const & lparams, expr const & type);
     constant_val(constant_val const & other):object_ref(other) {}
-    constant_val(constant_val && other):object_ref(std::move(other)) {}
+    constant_val(constant_val && other) noexcept:object_ref(std::move(other)) {}
     constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; }
-    constant_val & operator=(constant_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    constant_val & operator=(constant_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
     names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
     expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@@ -79,9 +79,9 @@ class axiom_val : public object_ref {
 public:
     axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe);
     axiom_val(axiom_val const & other):object_ref(other) {}
-    axiom_val(axiom_val && other):object_ref(std::move(other)) {}
+    axiom_val(axiom_val && other) noexcept:object_ref(std::move(other)) {}
     axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
-    axiom_val & operator=(axiom_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    axiom_val & operator=(axiom_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -105,9 +105,9 @@ class definition_val : public object_ref {
 public:
     definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all);
     definition_val(definition_val const & other):object_ref(other) {}
-    definition_val(definition_val && other):object_ref(std::move(other)) {}
+    definition_val(definition_val && other) noexcept:object_ref(std::move(other)) {}
     definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
-    definition_val & operator=(definition_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    definition_val & operator=(definition_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -128,9 +128,9 @@ class theorem_val : public object_ref {
 public:
     theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
     theorem_val(theorem_val const & other):object_ref(other) {}
-    theorem_val(theorem_val && other):object_ref(std::move(other)) {}
+    theorem_val(theorem_val && other) noexcept:object_ref(std::move(other)) {}
     theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
-    theorem_val & operator=(theorem_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    theorem_val & operator=(theorem_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -148,9 +148,9 @@ class opaque_val : public object_ref {
 public:
     opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all);
     opaque_val(opaque_val const & other):object_ref(other) {}
-    opaque_val(opaque_val && other):object_ref(std::move(other)) {}
+    opaque_val(opaque_val && other) noexcept:object_ref(std::move(other)) {}
     opaque_val & operator=(opaque_val const & other) { object_ref::operator=(other); return *this; }
-    opaque_val & operator=(opaque_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    opaque_val & operator=(opaque_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -179,9 +179,9 @@ class inductive_type : public object_ref {
 public:
     inductive_type(name const & id, expr const & type, constructors const & cnstrs);
     inductive_type(inductive_type const & other):object_ref(other) {}
-    inductive_type(inductive_type && other):object_ref(std::move(other)) {}
+    inductive_type(inductive_type && other) noexcept:object_ref(std::move(other)) {}
     inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; }
-    inductive_type & operator=(inductive_type && other) { object_ref::operator=(std::move(other)); return *this; }
+    inductive_type & operator=(inductive_type && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
     expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
     constructors const & get_cnstrs() const { return static_cast<constructors const &>(cnstr_get_ref(*this, 2)); }
@@ -205,7 +205,7 @@ class declaration : public object_ref {
 public:
     declaration();
     declaration(declaration const & other):object_ref(other) {}
-    declaration(declaration && other):object_ref(std::move(other)) {}
+    declaration(declaration && other) noexcept:object_ref(std::move(other)) {}
     /* low-level constructors */
     explicit declaration(object * o):object_ref(o) {}
     explicit declaration(b_obj_arg o, bool b):object_ref(o, b) {}
@@ -213,7 +213,7 @@ public:
     declaration_kind kind() const { return static_cast<declaration_kind>(obj_tag(raw())); }
 
     declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; }
-    declaration & operator=(declaration && other) { object_ref::operator=(std::move(other)); return *this; }
+    declaration & operator=(declaration && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); }
 
@@ -263,10 +263,10 @@ declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
 class inductive_decl : public object_ref {
 public:
     inductive_decl(inductive_decl const & other):object_ref(other) {}
-    inductive_decl(inductive_decl && other):object_ref(std::move(other)) {}
+    inductive_decl(inductive_decl && other) noexcept:object_ref(std::move(other)) {}
     inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); }
     inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; }
-    inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(std::move(other)); return *this; }
+    inductive_decl & operator=(inductive_decl && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(raw(), 0)); }
     nat const & get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 1)); }
     inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_get_ref(raw(), 2)); }
@@ -290,9 +290,9 @@ public:
     inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
                   unsigned nindices, names const & all, names const & cnstrs, unsigned nnested, bool is_rec, bool is_unsafe, bool is_reflexive);
     inductive_val(inductive_val const & other):object_ref(other) {}
-    inductive_val(inductive_val && other):object_ref(std::move(other)) {}
+    inductive_val(inductive_val && other) noexcept:object_ref(std::move(other)) {}
     inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
-    inductive_val & operator=(inductive_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    inductive_val & operator=(inductive_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
     unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@@ -317,9 +317,9 @@ class constructor_val : public object_ref {
 public:
     constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe);
     constructor_val(constructor_val const & other):object_ref(other) {}
-    constructor_val(constructor_val && other):object_ref(std::move(other)) {}
+    constructor_val(constructor_val && other) noexcept:object_ref(std::move(other)) {}
     constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
-    constructor_val & operator=(constructor_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    constructor_val & operator=(constructor_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_induct() const { return static_cast<name const &>(cnstr_get_ref(*this, 1)); }
     unsigned get_cidx() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@@ -338,9 +338,9 @@ class recursor_rule : public object_ref {
 public:
     recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs);
     recursor_rule(recursor_rule const & other):object_ref(other) {}
-    recursor_rule(recursor_rule && other):object_ref(std::move(other)) {}
+    recursor_rule(recursor_rule && other) noexcept:object_ref(std::move(other)) {}
     recursor_rule & operator=(recursor_rule const & other) { object_ref::operator=(other); return *this; }
-    recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(std::move(other)); return *this; }
+    recursor_rule & operator=(recursor_rule && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     name const & get_cnstr() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
     unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
     expr const & get_rhs() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@@ -365,9 +365,9 @@ public:
                  names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
                  unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe);
     recursor_val(recursor_val const & other):object_ref(other) {}
-    recursor_val(recursor_val && other):object_ref(std::move(other)) {}
+    recursor_val(recursor_val && other) noexcept:object_ref(std::move(other)) {}
     recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
-    recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    recursor_val & operator=(recursor_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     name const & get_major_induct() const;
@@ -398,9 +398,9 @@ class quot_val : public object_ref {
 public:
     quot_val(name const & n, names const & lparams, expr const & type, quot_kind k);
     quot_val(quot_val const & other):object_ref(other) {}
-    quot_val(quot_val && other):object_ref(std::move(other)) {}
+    quot_val(quot_val && other) noexcept:object_ref(std::move(other)) {}
     quot_val & operator=(quot_val const & other) { object_ref::operator=(other); return *this; }
-    quot_val & operator=(quot_val && other) { object_ref::operator=(std::move(other)); return *this; }
+    quot_val & operator=(quot_val && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -434,14 +434,14 @@ public:
     constant_info(constructor_val const & v);
     constant_info(recursor_val const & v);
     constant_info(constant_info const & other):object_ref(other) {}
-    constant_info(constant_info && other):object_ref(std::move(other)) {}
+    constant_info(constant_info && other) noexcept:object_ref(std::move(other)) {}
     explicit constant_info(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit constant_info(obj_arg o):object_ref(o) {}
 
     constant_info_kind kind() const { return static_cast<constant_info_kind>(cnstr_tag(raw())); }
 
     constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; }
-    constant_info & operator=(constant_info && other) { object_ref::operator=(std::move(other)); return *this; }
+    constant_info & operator=(constant_info && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     friend bool is_eqp(constant_info const & d1, constant_info const & d2) { return d1.raw() == d2.raw(); }
 
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 7a7073be32..a0bed6203f 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -29,7 +29,7 @@ namespace lean {
 class diagnostics : public object_ref {
 public:
     diagnostics(diagnostics const & other):object_ref(other) {}
-    diagnostics(diagnostics && other):object_ref(std::move(other)) {}
+    diagnostics(diagnostics && other) noexcept:object_ref(std::move(other)) {}
     explicit diagnostics(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit diagnostics(obj_arg o):object_ref(o) {}
     ~diagnostics() {}
@@ -74,13 +74,13 @@ class LEAN_EXPORT environment : public object_ref {
     environment add_inductive(declaration const & d) const;
 public:
     environment(environment const & other):object_ref(other) {}
-    environment(environment && other):object_ref(std::move(other)) {}
+    environment(environment && other) noexcept:object_ref(std::move(other)) {}
     explicit environment(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit environment(obj_arg o):object_ref(o) {}
     ~environment() {}
 
     environment & operator=(environment const & other) { object_ref::operator=(other); return *this; }
-    environment & operator=(environment && other) { object_ref::operator=(std::move(other)); return *this; }
+    environment & operator=(environment && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     diagnostics get_diag() const;
     environment set_diag(diagnostics const & diag) const;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 526d2792e9..bcf83b97aa 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -50,9 +50,9 @@ public:
     explicit literal(nat const & v);
     literal():literal(0u) {}
     literal(literal const & other):object_ref(other) {}
-    literal(literal && other):object_ref(std::move(other)) {}
+    literal(literal && other) noexcept:object_ref(std::move(other)) {}
     literal & operator=(literal const & other) { object_ref::operator=(other); return *this; }
-    literal & operator=(literal && other) { object_ref::operator=(std::move(other)); return *this; }
+    literal & operator=(literal && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     static literal_kind kind(object * o) { return static_cast<literal_kind>(cnstr_tag(o)); }
     literal_kind kind() const { return kind(raw()); }
@@ -83,7 +83,7 @@ inductive Expr
 */
 enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj };
 class expr : public object_ref {
-    explicit expr(object_ref && o):object_ref(o) {}
+    explicit expr(object_ref && o) noexcept:object_ref(o) {}
 
     friend expr mk_lit(literal const & lit);
     friend expr mk_mdata(kvmap const & d, expr const & e);
@@ -100,14 +100,14 @@ class expr : public object_ref {
 public:
     expr();
     expr(expr const & other):object_ref(other) {}
-    expr(expr && other):object_ref(std::move(other)) {}
+    expr(expr && other) noexcept:object_ref(std::move(other)) {}
     explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit expr(obj_arg o):object_ref(o) {}
     static expr_kind kind(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
     expr_kind kind() const { return kind(raw()); }
 
     expr & operator=(expr const & other) { object_ref::operator=(other); return *this; }
-    expr & operator=(expr && other) { object_ref::operator=(std::move(other)); return *this; }
+    expr & operator=(expr && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
 };
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 0739ab6e8f..bc3b7d93b5 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -36,21 +36,21 @@ class level : public object_ref {
     friend level mk_imax_core(level const & l1, level const & l2);
     friend level mk_univ_param(name const & n);
     friend level mk_univ_mvar(name const & n);
-    explicit level(object_ref && o):object_ref(o) {}
+    explicit level(object_ref && o) noexcept:object_ref(o) {}
 public:
     /** \brief Universe zero */
     level();
     explicit level(obj_arg o):object_ref(o) {}
     explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
     level(level const & other):object_ref(other) {}
-    level(level && other):object_ref(std::move(other)) {}
+    level(level && other) noexcept:object_ref(std::move(other)) {}
     level_kind kind() const {
       return lean_is_scalar(raw()) ? level_kind::Zero : static_cast<level_kind>(lean_ptr_tag(raw()));
     }
     unsigned hash() const;
 
     level & operator=(level const & other) { object_ref::operator=(other); return *this; }
-    level & operator=(level && other) { object_ref::operator=(std::move(other)); return *this; }
+    level & operator=(level && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }
 
diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h
index 500d62a03c..614339d9e8 100644
--- a/src/kernel/local_ctx.h
+++ b/src/kernel/local_ctx.h
@@ -27,11 +27,11 @@ class local_decl : public object_ref {
 public:
     local_decl();
     local_decl(local_decl const & other):object_ref(other) {}
-    local_decl(local_decl && other):object_ref(std::move(other)) {}
+    local_decl(local_decl && other) noexcept:object_ref(std::move(other)) {}
     local_decl(obj_arg o):object_ref(o) {}
     local_decl(b_obj_arg o, bool):object_ref(o, true) {}
     local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
-    local_decl & operator=(local_decl && other) { object_ref::operator=(std::move(other)); return *this; }
+    local_decl & operator=(local_decl && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
     unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
     name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
@@ -54,9 +54,9 @@ public:
     explicit local_ctx(obj_arg o):object_ref(o) {}
     local_ctx(b_obj_arg o, bool):object_ref(o, true) {}
     local_ctx(local_ctx const & other):object_ref(other) {}
-    local_ctx(local_ctx && other):object_ref(std::move(other)) {}
+    local_ctx(local_ctx && other) noexcept:object_ref(std::move(other)) {}
     local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; }
-    local_ctx & operator=(local_ctx && other) { object_ref::operator=(std::move(other)); return *this; }
+    local_ctx & operator=(local_ctx && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     bool empty() const;
 
diff --git a/src/library/elab_environment.h b/src/library/elab_environment.h
index a8ed8f9061..e457e34569 100644
--- a/src/library/elab_environment.h
+++ b/src/library/elab_environment.h
@@ -12,13 +12,13 @@ namespace lean {
 class LEAN_EXPORT elab_environment : public object_ref {
 public:
     elab_environment(elab_environment const & other):object_ref(other) {}
-    elab_environment(elab_environment && other):object_ref(std::move(other)) {}
+    elab_environment(elab_environment && other) noexcept:object_ref(std::move(other)) {}
     explicit elab_environment(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit elab_environment(obj_arg o):object_ref(o) {}
     ~elab_environment() {}
 
     elab_environment & operator=(elab_environment const & other) { object_ref::operator=(other); return *this; }
-    elab_environment & operator=(elab_environment && other) { object_ref::operator=(std::move(other)); return *this; }
+    elab_environment & operator=(elab_environment && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     /** \brief Return information for the constant with name \c n (if it is defined in this environment). */
     optional<constant_info> find(name const & n) const { return to_kernel_env().find(n); };
diff --git a/src/library/projection.h b/src/library/projection.h
index 89e88d5004..d9d237c8f5 100644
--- a/src/library/projection.h
+++ b/src/library/projection.h
@@ -24,13 +24,13 @@ public:
     projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit);
     projection_info():projection_info(name(), 0, 0, false) {}
     projection_info(projection_info const & other):object_ref(other) {}
-    projection_info(projection_info && other):object_ref(std::move(other)) {}
+    projection_info(projection_info && other) noexcept:object_ref(std::move(other)) {}
     /* low-level constructors */
     explicit projection_info(object * o):object_ref(o) {}
     explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit projection_info(object_ref const & o):object_ref(o) {}
     projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; }
-    projection_info & operator=(projection_info && other) { object_ref::operator=(std::move(other)); return *this; }
+    projection_info & operator=(projection_info && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     name const & get_constructor() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
     unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
     unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
diff --git a/src/runtime/array_ref.h b/src/runtime/array_ref.h
index 468ca77340..a7c2ede465 100644
--- a/src/runtime/array_ref.h
+++ b/src/runtime/array_ref.h
@@ -28,12 +28,12 @@ public:
     array_ref(b_obj_arg o, bool b):object_ref(o, b) {}
     array_ref():object_ref(array_mk_empty()) {}
     array_ref(array_ref const & other):object_ref(other) {}
-    array_ref(array_ref && other):object_ref(std::move(other)) {}
+    array_ref(array_ref && other) noexcept:object_ref(std::move(other)) {}
     array_ref(std::initializer_list<T> const & elems):object_ref(to_array(elems)) {}
     array_ref(buffer<T> const & elems):object_ref(to_array(elems)) {}
 
     array_ref & operator=(array_ref const & other) { object_ref::operator=(other); return *this; }
-    array_ref & operator=(array_ref && other) { object_ref::operator=(std::move(other)); return *this; }
+    array_ref & operator=(array_ref && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     size_t size() const { return array_size(raw()); }
 
diff --git a/src/runtime/list_ref.h b/src/runtime/list_ref.h
index 1b5f163c56..709c75c937 100644
--- a/src/runtime/list_ref.h
+++ b/src/runtime/list_ref.h
@@ -23,7 +23,7 @@ public:
     explicit list_ref(list_ref<T> const * l) { if (l) *this = *l; }
     list_ref(T const & h, list_ref<T> const & t):object_ref(mk_cnstr(1, h.raw(), t.raw())) { inc(h.raw()); inc(t.raw()); }
     list_ref(list_ref const & other):object_ref(other) {}
-    list_ref(list_ref && other):object_ref(std::move(other)) {}
+    list_ref(list_ref && other) noexcept:object_ref(std::move(other)) {}
     template<typename It> list_ref(It const & begin, It const & end):list_ref() {
         auto it = end;
         while (it != begin) {
@@ -35,7 +35,7 @@ public:
     list_ref(buffer<T> const & b):list_ref(b.begin(), b.end()) {}
 
     list_ref & operator=(list_ref const & other) { object_ref::operator=(other); return *this; }
-    list_ref & operator=(list_ref && other) { object_ref::operator=(std::move(other)); return *this; }
+    list_ref & operator=(list_ref && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     explicit operator bool() const { return !is_scalar(raw()); }
     friend bool is_nil(list_ref const & l) { return is_scalar(l.raw()); }
diff --git a/src/runtime/object_ref.h b/src/runtime/object_ref.h
index e543384dc3..6b712ff4d6 100644
--- a/src/runtime/object_ref.h
+++ b/src/runtime/object_ref.h
@@ -20,7 +20,7 @@ public:
     explicit object_ref(obj_arg o):m_obj(o) {}
     object_ref(b_obj_arg o, bool):m_obj(o) { inc(o); }
     object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
-    object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }
+    object_ref(object_ref && s) noexcept:m_obj(s.m_obj) { s.m_obj = box(0); }
     ~object_ref() { dec(m_obj); }
     object_ref & operator=(object_ref const & s) {
         inc(s.m_obj);
diff --git a/src/runtime/option_ref.h b/src/runtime/option_ref.h
index 5191bca14e..1e6472260a 100644
--- a/src/runtime/option_ref.h
+++ b/src/runtime/option_ref.h
@@ -16,14 +16,14 @@ public:
     option_ref(b_obj_arg o, bool b):object_ref(o, b) {}
     option_ref():object_ref(box(0)) {}
     option_ref(option_ref const & other):object_ref(other) {}
-    option_ref(option_ref && other):object_ref(std::move(other)) {}
+    option_ref(option_ref && other) noexcept:object_ref(std::move(other)) {}
     explicit option_ref(T const & a):object_ref(mk_cnstr(1, a.raw())) { inc(a.raw()); }
     explicit option_ref(T const * a) { if (a) *this = option_ref(*a); }
     explicit option_ref(option_ref<T> const * o) { if (o) *this = *o; }
     explicit option_ref(optional<T> const & o):option_ref(o ? &*o : nullptr) {}
 
     option_ref & operator=(option_ref const & other) { object_ref::operator=(other); return *this; }
-    option_ref & operator=(option_ref && other) { object_ref::operator=(std::move(other)); return *this; }
+    option_ref & operator=(option_ref && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     explicit operator bool() const { return !is_scalar(raw()); }
     optional<T> get() const { return *this ? some(static_cast<T const &>(cnstr_get_ref(*this, 0))) : optional<T>(); }
diff --git a/src/runtime/optional.h b/src/runtime/optional.h
index 995fb31859..e3ea57f2f1 100644
--- a/src/runtime/optional.h
+++ b/src/runtime/optional.h
@@ -29,7 +29,7 @@ public:
         if (m_some)
             new (&m_value) T(other.m_value);
     }
-    optional(optional && other):m_some(other.m_some) {
+    optional(optional && other) noexcept(std::is_nothrow_move_constructible<T>::value):m_some(other.m_some) {
         if (other.m_some)
             new (&m_value) T(std::move(other.m_value));
     }
@@ -78,7 +78,7 @@ public:
             new (&m_value) T(other.m_value);
         return *this;
     }
-    optional& operator=(optional && other) {
+    optional& operator=(optional && other) noexcept {
         lean_assert(this != &other);
         if (m_some)
             m_value.~T();
@@ -94,7 +94,7 @@ public:
         new (&m_value) T(other);
         return *this;
     }
-    optional& operator=(T && other) {
+    optional& operator=(T && other) noexcept {
         if (m_some)
             m_value.~T();
         m_some = true;
@@ -130,9 +130,9 @@ template<> class optional<P> {                                          \
 public:                                                                 \
     optional():m_value(nullptr) {}                                      \
     optional(optional const & other):m_value(other.m_value) {}          \
-    optional(optional && other):m_value(std::move(other.m_value)) {} \
+    optional(optional && other) noexcept:m_value(std::move(other.m_value)) {} \
     explicit optional(P const & v):m_value(v) {}                        \
-    explicit optional(P && v):m_value(std::move(v)) {}            \
+    explicit optional(P && v) noexcept(std::is_nothrow_move_constructible<P>::value):m_value(std::move(v)) {}            \
                                                                         \
     explicit operator bool() const { return m_value.m_ptr != nullptr; } \
     P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \
@@ -142,9 +142,9 @@ public:                                                                 \
     P const & value() const { lean_assert(m_value.m_ptr); return m_value; } \
     P & value() { lean_assert(m_value.m_ptr); return m_value; }         \
     optional & operator=(optional const & other) { m_value = other.m_value; return *this; } \
-    optional& operator=(optional && other) { m_value = std::move(other.m_value); return *this; } \
+    optional& operator=(optional && other) noexcept { m_value = std::move(other.m_value); return *this; } \
     optional& operator=(P const & other) { m_value = other; return *this; } \
-    optional& operator=(P && other) { m_value = std::move(other); return *this; } \
+    optional& operator=(P && other) noexcept { m_value = std::move(other); return *this; } \
     friend bool operator==(optional const & o1, optional const & o2) {  \
         return static_cast<bool>(o1) == static_cast<bool>(o2) && (!o1 || o1.m_value == o2.m_value); \
     }                                                                   \
diff --git a/src/runtime/pair_ref.h b/src/runtime/pair_ref.h
index d09929930a..7ee83acc41 100644
--- a/src/runtime/pair_ref.h
+++ b/src/runtime/pair_ref.h
@@ -16,9 +16,9 @@ public:
     explicit pair_ref(b_obj_arg o, bool b):object_ref(o, b) {}
     pair_ref(T1 const & a, T2 const & b):object_ref(mk_cnstr(0, a.raw(), b.raw())) { inc(a.raw()); inc(b.raw()); }
     pair_ref(pair_ref const & other):object_ref(other) {}
-    pair_ref(pair_ref && other):object_ref(std::move(other)) {}
+    pair_ref(pair_ref && other) noexcept:object_ref(std::move(other)) {}
     pair_ref & operator=(pair_ref const & other) { object_ref::operator=(other); return *this; }
-    pair_ref & operator=(pair_ref && other) { object_ref::operator=(std::move(other)); return *this; }
+    pair_ref & operator=(pair_ref && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     T1 const & fst() const { return static_cast<T1 const &>(cnstr_get_ref(*this, 0)); }
     T2 const & snd() const { return static_cast<T2 const &>(cnstr_get_ref(*this, 1)); }
diff --git a/src/runtime/string_ref.h b/src/runtime/string_ref.h
index dd9fb726cb..059478ad7a 100644
--- a/src/runtime/string_ref.h
+++ b/src/runtime/string_ref.h
@@ -17,11 +17,11 @@ public:
     explicit string_ref(std::string const & s):object_ref(mk_string(s)) {}
     explicit string_ref(sstream const & strm):string_ref(strm.str()) {}
     string_ref(string_ref const & other):object_ref(other) {}
-    string_ref(string_ref && other):object_ref(std::move(other)) {}
+    string_ref(string_ref && other) noexcept:object_ref(std::move(other)) {}
     explicit string_ref(obj_arg o):object_ref(o) {}
     string_ref(b_obj_arg o, bool b):object_ref(o, b) {}
     string_ref & operator=(string_ref const & other) { object_ref::operator=(other); return *this; }
-    string_ref & operator=(string_ref && other) { object_ref::operator=(std::move(other)); return *this; }
+    string_ref & operator=(string_ref && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     /* Number of bytes used to store the string in UTF8.
        Remark: it does not include the null character added in the end to make it efficient to
        convert to C string. */
diff --git a/src/runtime/thread.h b/src/runtime/thread.h
index ce721619e4..1baa4b25b6 100644
--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@ -83,13 +83,13 @@ class atomic {
     T m_value;
 public:
     atomic(T const & v = T()):m_value(v) {}
-    atomic(T && v):m_value(std::forward<T>(v)) {}
+    atomic(T && v) noexcept(std::is_nothrow_move_constructible<T>::value):m_value(std::move(v)) {}
     atomic(atomic const & v):m_value(v.m_value) {}
-    atomic(atomic && v):m_value(std::forward<T>(v.m_value)) {}
+    atomic(atomic && v) noexcept(std::is_nothrow_move_constructible<T>::value):m_value(std::move(v.m_value)) {}
     atomic & operator=(T const & v) { m_value = v; return *this; }
-    atomic & operator=(T && v) { m_value = std::forward<T>(v); return *this; }
+    atomic & operator=(T && v) { m_value = std::move(v); return *this; }
     atomic & operator=(atomic const & v) { m_value = v.m_value; return *this; }
-    atomic & operator=(atomic && v) { m_value = std::forward<T>(v.m_value); return *this; }
+    atomic & operator=(atomic && v) { m_value = std::move(v.m_value); return *this; }
     operator T() const { return m_value; }
     void store(T const & v) { m_value = v; }
     T load() const { return m_value; }
diff --git a/src/util/kvmap.h b/src/util/kvmap.h
index 5c22c61332..6c1b698aca 100644
--- a/src/util/kvmap.h
+++ b/src/util/kvmap.h
@@ -30,9 +30,9 @@ public:
     explicit data_value(name const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::Name), v.raw())) { inc(v.raw()); }
     data_value():data_value(false) {}
     data_value(data_value const & other):object_ref(other) {}
-    data_value(data_value && other):object_ref(std::move(other)) {}
+    data_value(data_value && other) noexcept:object_ref(std::move(other)) {}
     data_value & operator=(data_value const & other) { object_ref::operator=(other); return *this; }
-    data_value & operator=(data_value && other) { object_ref::operator=(std::move(other)); return *this; }
+    data_value & operator=(data_value && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
 
     data_value_kind kind() const { return static_cast<data_value_kind>(cnstr_tag(raw())); }
     string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
diff --git a/src/util/list.h b/src/util/list.h
index 2ba38a989a..ccd51ba8f6 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -40,7 +40,7 @@ public:
     list(T const & h, list const & t):m_ptr(new cell(h, t)) {}
     explicit list(T const & h):m_ptr(new cell(h, list())) {}
     list(list const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    list(list&& s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    list(list&& s) noexcept:m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     list(std::initializer_list<T> const & l):list() {
         auto it = l.end();
         while (it != l.begin()) {
diff --git a/src/util/name.h b/src/util/name.h
index b92b6a3608..63e161607b 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -61,7 +61,7 @@ public:
     static int cmp_core(object * o1, object * o2);
     size_t size_core(bool unicode) const;
 private:
-    explicit name(object_ref && r):object_ref(r) {}
+    explicit name(object_ref && r) noexcept:object_ref(r) {}
 public:
     name():object_ref(box(static_cast<unsigned>(name_kind::ANONYMOUS))) {}
     explicit name(obj_arg o):object_ref(o) {}
@@ -74,7 +74,7 @@ public:
     name(std::string const & s):name(name(), string_ref(s)) {}
     name(string_ref const & s):name(name(), s) {}
     name(name const & other):object_ref(other) {}
-    name(name && other):object_ref(std::move(other)) {}
+    name(name && other) noexcept:object_ref(std::move(other)) {}
     /**
        \brief Create a hierarchical name using the given strings.
        Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
@@ -97,7 +97,7 @@ public:
     */
     static name mk_internal_unique_name();
     name & operator=(name const & other) { object_ref::operator=(other); return *this; }
-    name & operator=(name && other) { object_ref::operator=(std::move(other)); return *this; }
+    name & operator=(name && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     static uint64_t hash(b_obj_arg n) {
        lean_assert(lean_name_hash(n) == lean_name_hash_exported_b(n));
        return lean_name_hash(n);
diff --git a/src/util/nat.h b/src/util/nat.h
index 8035a9cd5f..453fac8ccc 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -27,10 +27,10 @@ public:
     static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); }
 
     nat(nat const & other):object_ref(other) {}
-    nat(nat && other):object_ref(std::move(other)) {}
+    nat(nat && other) noexcept:object_ref(std::move(other)) {}
 
     nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
-    nat & operator=(nat && other) { object_ref::operator=(std::move(other)); return *this; }
+    nat & operator=(nat && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
     bool is_small() const { return is_scalar(raw()); }
     size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
     bool is_zero() const { return is_small() && get_small_value() == 0; }
diff --git a/src/util/options.h b/src/util/options.h
index a9240ab359..75c9ea1f47 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -19,7 +19,7 @@ public:
     explicit options(obj_arg o):m_value(o) {}
     options(b_obj_arg o, bool v):m_value(o, v) {}
     options(options const & o):m_value(o.m_value) {}
-    options(options && o):m_value(std::move(o.m_value)) {}
+    options(options && o) noexcept:m_value(std::move(o.m_value)) {}
     options(name const & n, bool v) { *this = update(n, v); }
     options & operator=(options const & o) { m_value = o.m_value; return *this; }
 
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index b6e4733ec5..a72e46b4f2 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -43,7 +43,7 @@ class rb_tree : private CMP {
         node():m_ptr(nullptr) {}
         node(node_cell * ptr):m_ptr(ptr) { if (m_ptr) ptr->inc_ref(); }
         node(node const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-        node(node && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+        node(node && s) noexcept:m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
         ~node() { if (m_ptr) m_ptr->dec_ref(); }
         node & operator=(node const & n) { LEAN_COPY_REF(n); }
         node & operator=(node&& n) { LEAN_MOVE_REF(n); }
@@ -385,7 +385,7 @@ class rb_tree : private CMP {
 public:
     rb_tree(CMP const & cmp = CMP()):CMP(cmp) {}
     rb_tree(rb_tree const & s):CMP(s), m_root(s.m_root) {}
-    rb_tree(rb_tree && s):CMP(s), m_root(s.m_root) {}
+    rb_tree(rb_tree && s) noexcept:CMP(s), m_root(s.m_root) {}
     explicit rb_tree(buffer<T> const & s) {
         for (auto const & v : s)
             insert(v);