diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 2e0d27bc24..fdde045c93 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -439,14 +439,16 @@ public:
             type_checker tc(m_st, m_lctx);
             expr type = tc.whnf(tc.infer(e));
             if (is_sort(type)) {
-                // Types are not pre-processed
+                /* Types are not pre-processed */
                 return cache_result(e, e, shared);
             } else if (tc.is_prop(type)) {
-                // We replace proofs using `lc_proof` constant
+                /* We replace proofs using `lc_proof` constant */
                 expr r = mk_app(mk_constant(get_lc_proof_name()), type);
                 return cache_result(e, r, shared);
             } else if (is_pi(type)) {
-                // Functions that return types are not pre-processed
+                /* Functions that return types are not pre-processed.
+                   This is a partial (and quick) check since we are not using
+                   `whnf` on nested terms. */
                 while (is_pi(type))
                     type = binding_body(type);
                 if (is_sort(type))