From 1b9e2efb0ca71aed73d1b9bc86a25040cdc37e0b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Apr 2014 14:01:44 -0700 Subject: [PATCH] fix(kernel/environment): relax normalizer_extesion interface Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 2 +- src/kernel/environment.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index a1691cb1d..06c7c4c03 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -16,7 +16,7 @@ namespace lean { */ class noop_normalizer_extension : public normalizer_extension { public: - virtual optional operator()(expr const &, extension_context const &) const { + virtual optional operator()(expr const &, extension_context &) const { return none_expr(); } }; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index fcc7a102e..0a83e3229 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -31,7 +31,7 @@ class certified_definition; class normalizer_extension { public: virtual ~normalizer_extension() {} - virtual optional operator()(expr const & e, extension_context const & ctx) const = 0; + virtual optional operator()(expr const & e, extension_context & ctx) const = 0; }; /**