From cdccca93162d94b4fd82c8780166bf1782227d51 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Aug 2013 10:48:38 -0700 Subject: [PATCH] Rename builtin operator if-then-else Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index ebe790b6a..4ceacc704 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -128,7 +128,7 @@ bool is_false(expr const & e) { // ======================================= // If-then-else builtin operator -static name g_ite_name = name{"builtin", "if"}; +static name g_ite_name("ite"); static format g_ite_fmt(g_ite_name); class ite_fn_value : public value { expr m_type; @@ -161,7 +161,7 @@ public: virtual format pp() const { return g_ite_fmt; } virtual unsigned hash() const { return 27; } }; -char const * ite_fn_value::g_kind = "builtin::if"; +char const * ite_fn_value::g_kind = "ite"; MK_BUILTIN(ite_fn, ite_fn_value); // =======================================