diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 172fcfb77..8a8864c07 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -134,7 +134,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
                                           opaque, rec_decl.get_module_idx(), use_conv_opt);
         new_env = module::add(new_env, check(new_env, new_d));
         new_env = set_reducible(new_env, proj_name, reducible_status::On);
-        new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i);
+        new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);
         expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
         intro_type        = instantiate(binding_body(intro_type), proj);
         i++;
diff --git a/src/library/projection.cpp b/src/library/projection.cpp
index 881aa5f84..cd2bc5618 100644
--- a/src/library/projection.cpp
+++ b/src/library/projection.cpp
@@ -39,15 +39,16 @@ static environment update(environment const & env, projection_ext const & ext) {
 
 static std::string * g_proj_key = nullptr;
 
-static environment save_projection_info_core(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i) {
+static environment save_projection_info_core(environment const & env, name const & p, name const & mk, unsigned nparams,
+                                             unsigned i, bool inst_implicit) {
     projection_ext ext = get_extension(env);
-    ext.m_info.insert(p, projection_info(mk, nparams, i));
+    ext.m_info.insert(p, projection_info(mk, nparams, i, inst_implicit));
     return update(env, ext);
 }
 
-environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i) {
-    environment new_env = save_projection_info_core(env, p, mk, nparams, i);
-    return module::add(new_env, *g_proj_key, [=](serializer & s) { s << p << mk << nparams << i; });
+environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) {
+    environment new_env = save_projection_info_core(env, p, mk, nparams, i, inst_implicit);
+    return module::add(new_env, *g_proj_key, [=](serializer & s) { s << p << mk << nparams << i << inst_implicit; });
 }
 
 projection_info const * get_projection_info(environment const & env, name const & p) {
@@ -58,10 +59,10 @@ projection_info const * get_projection_info(environment const & env, name const
 static void projection_info_reader(deserializer & d, module_idx, shared_environment & senv,
                                    std::function<void(asynch_update_fn const &)> &,
                                    std::function<void(delayed_update_fn const &)> &) {
-    name p, mk; unsigned nparams, i;
-    d >> p >> mk >> nparams >> i;
+    name p, mk; unsigned nparams, i; bool inst_implicit;
+    d >> p >> mk >> nparams >> i >> inst_implicit;
     senv.update([=](environment const & env) -> environment {
-            return save_projection_info_core(env, p, mk, nparams, i);
+            return save_projection_info_core(env, p, mk, nparams, i, inst_implicit);
         });
 }
 
diff --git a/src/library/projection.h b/src/library/projection.h
index 0e630e1c5..688bb9cf8 100644
--- a/src/library/projection.h
+++ b/src/library/projection.h
@@ -20,20 +20,22 @@ namespace lean {
     We also use this information in the rewriter/simplifier.
 */
 struct projection_info {
-    name     m_constructor; // mk in the rule above
-    unsigned m_nparams;     // number of parameters of the inductive datatype
-    unsigned m_i;           // i in the rule above
+    name     m_constructor;   // mk in the rule above
+    unsigned m_nparams;       // number of parameters of the inductive datatype
+    unsigned m_i;             // i in the rule above
+    bool     m_inst_implicit; // true if it is the projection of a "class"
 
     projection_info() {}
-    projection_info(name const & c, unsigned nparams, unsigned i):
-        m_constructor(c), m_nparams(nparams), m_i(i) {}
+    projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit):
+        m_constructor(c), m_nparams(nparams), m_i(i), m_inst_implicit(inst_implicit) {}
 };
 
 /** \brief Mark \c p as a projection in the given environment and store that
     \c mk is the constructor associated with it, \c nparams is the number of parameters, and
     \c i says that \c p is the i-th projection.
 */
-environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i);
+environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i,
+                                 bool inst_implicit);
 
 /** \brief If \c p is a projection in the given environment, then return the information
     associated with it (constructor, number of parameters, and index).