From 0c9317b16738331100d8fe5b58bb38ee3460587f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Aug 2014 20:25:06 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): add flyinfo for placeholders Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; }