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; }; /**