From 1bdf7ae55a365108521e5d2bca893c2fd049c4eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Feb 2015 19:25:56 -0800 Subject: [PATCH] feat(kernel/default_converter): make norm_ext virtual --- src/kernel/default_converter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h index 5dfb334e0..eb7547a08 100644 --- a/src/kernel/default_converter.h +++ b/src/kernel/default_converter.h @@ -27,11 +27,11 @@ protected: delayed_justification * m_jst; virtual bool may_reduce_later(expr const & e); + virtual optional> norm_ext(expr const & e); pair infer_type(expr const & e) { return converter::infer_type(*m_tc, e); } constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j); optional expand_macro(expr const & m); - optional> norm_ext(expr const & e); optional d_norm_ext(expr const & e, constraint_seq & cs); expr whnf_core(expr const & e); expr unfold_name_core(expr e, unsigned w);