diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index ca9eae6138..0134dbfd16 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -405,7 +405,8 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
     if r.isAppOf ``isTrue then
       -- Success!
       -- While we have a proof from reduction, we do not embed it in the proof term,
-      -- and instead we let the kernel recompute it during type checking from the following more efficient term.
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
       let rflPrf ← mkEqRefl (toExpr true)
       return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
     else
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 0a07d45880..54b7192dcc 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -1072,7 +1072,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
 
     // Very basic support for proofs by reflection. If `t` has no free variables and `s` is `Bool.true`,
     // we fully reduce `t` and check whether result is `s`.
-    // TODO: add metadata to control whether this optimization is used or not.
+    // This code path is taken in particular when using the `decide` tactic, which produces
+    // proof terms of the form `Eq.refl true : decide p = true`.
     if (!has_fvar(t) && is_constant(s, *g_bool_true)) {
         if (is_constant(whnf(t), *g_bool_true)) {
             return true;