From bdef7aaf40002cefa0b9573969e2f925fce341c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Apr 2015 14:21:53 -0700 Subject: [PATCH] feat(frontends/lean/pp): add check_system at pretty printer --- src/frontends/lean/pp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 6ae5d0df4f..f2a0fa5d12 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1136,6 +1136,7 @@ static bool is_pp_atomic(expr const & e) { } auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { + check_system("pretty printer"); if ((m_depth >= m_max_depth || m_num_steps > m_max_steps || (m_hide_full_terms && !ignore_hide && !has_expr_metavar_relaxed(e))) &&