diff --git a/doc/coding_style.md b/doc/coding_style.md
index b2a8ecae6c..3398d1d5f0 100644
--- a/doc/coding_style.md
+++ b/doc/coding_style.md
@@ -161,13 +161,13 @@ Similarly, we write `x < y + 1` instead of `x<y+1`.
 Google's C++ Style Guide
 ------------------------
 
-We are using a modified version of [Google's C++ Style Guide][google-style]. 
+We are using a modified version of [Google's C++ Style Guide][google-style].
 We also have our version of Google's style checker [cpplint.py][cpplint].
 You can run the checker over the codebase by typing:
 
     make style
-    
-If you use Ninja, you can check by ``ninja style``. It is also a part of testcases and can be run by 
+
+If you use Ninja, you can check by ``ninja style``. It is also a part of testcases and can be run by
 
     ctest -R style_check
 
@@ -193,6 +193,7 @@ If you use Ninja, you can check by ``ninja style``. It is also a part of testcas
  - Extra space before ``)``
  - Is this a non-const reference? If so, make const or use a pointer.
  - All parameters should be named in a function
+ - Do not use anonymous constructor notation (e.g., ``{a1, ..., an}``)
 
 Modified Features:
 
@@ -214,7 +215,7 @@ Modified Features:
     => *Allow* this if filename contains "tests/"
 
   - Include the directory when naming .h files
-  
+
     => *Allow* this if the included filename is "version.h" which is generated by cmake.
 
 [google-style]: http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2082fe63db..8835008aa4 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1877,13 +1877,12 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
         auto field_res   = find_field_fn(fn, s, s_type);
         expr proj, proj_type;
         if (field_res.m_ldecl) {
-            proj      = field_res.m_ldecl->mk_ref();
+            proj      = copy_tag(fn, field_res.m_ldecl->mk_ref());
             proj_type = field_res.m_ldecl->get_type();
         } else {
-            proj      = mk_constant(field_res.get_full_fname());
+            proj      = copy_tag(fn, mk_constant(field_res.get_full_fname()));
             proj_type = m_env.get(field_res.get_full_fname()).get_type();
         }
-        proj = copy_tag(fn, std::move(proj));
         buffer<expr> new_args;
         unsigned i       = 0;
         while (is_pi(proj_type)) {
@@ -2748,11 +2747,11 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons
         // search for "true" fields first, including in parent structures
         if (is_structure_like(m_env, const_name(I)))
             if (auto p = find_field(m_env, const_name(I), fname))
-                return {const_name(I), *p, fname};
+                return field_resolution(const_name(I), *p, fname);
         name full_fname = const_name(I) + fname;
         if (auto ldecl = m_ctx.lctx().find_local_decl_from_user_name(full_fname.replace_prefix(get_namespace(env()), {}))) {
             // recursive call
-            return {full_fname, ldecl};
+            return field_resolution(full_fname, ldecl);
         }
         if (!m_env.find(full_fname)) {
             auto pp_fn = mk_pp_ctx();