diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c7c627631..ba505a1e7 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1061,7 +1061,7 @@ public: } } } - if (is_constant(e) || is_local(e)) + if (is_constant(e) || is_local(e) || is_placeholder(e)) save_flyinfo_data(e, r); return r; }