diff --git a/src/library/elab_environment.h b/src/library/elab_environment.h index 8aa95e6016..a8ed8f9061 100644 --- a/src/library/elab_environment.h +++ b/src/library/elab_environment.h @@ -35,8 +35,6 @@ public: } environment to_kernel_env() const; - - // TODO: delete together with old compiler operator environment() const { return to_kernel_env(); } }; }