diff --git a/src/compiler/init_module.cpp b/src/compiler/init_module.cpp new file mode 100644 index 000000000..9f13c7f15 --- /dev/null +++ b/src/compiler/init_module.cpp @@ -0,0 +1,15 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "compiler/preprocess_rec.h" +namespace lean{ +void initialize_compiler_module() { + initialize_preprocess_rec(); +} +void finalize_compiler_module() { + finalize_preprocess_rec(); +} +} diff --git a/src/compiler/init_module.h b/src/compiler/init_module.h new file mode 100644 index 000000000..575bce624 --- /dev/null +++ b/src/compiler/init_module.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +void initialize_compiler_module(); +void finalize_compiler_module(); +}