From f7bc884ae82da50f1ba260eaea4affe7bbe33150 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Dec 2017 08:44:51 -0800 Subject: [PATCH] chore(kernel/type_checker): fix compilation warning msgs --- src/kernel/type_checker.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 8a7bcab50b..66882adde9 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -98,7 +98,7 @@ public: expr check_ignore_undefined_universes(expr const & e); virtual expr check(expr const & t) { return check_ignore_undefined_universes(t); } - bool is_trusted_only() const override { return m_trusted_only; } + virtual bool is_trusted_only() const { return m_trusted_only; } /** \brief Return true iff t is definitionally equal to s. */ virtual bool is_def_eq(expr const & t, expr const & s);