From 98a27c53de22ed4593379eb90f21f4fa33d9a8b2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 23 Aug 2015 07:49:06 -0700 Subject: [PATCH] refactor(api/env): use module procedures --- src/api/env.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/env.cpp b/src/api/env.cpp index 1af48f531..e1fc1e42d 100644 --- a/src/api/env.cpp +++ b/src/api/env.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "library/standard_kernel.h" #include "library/hott_kernel.h" +#include "library/module.h" #include "api/decl.h" #include "api/string.h" #include "api/exception.h" @@ -29,7 +30,7 @@ lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exceptio LEAN_TRY; check_nonnull(e); check_nonnull(u); - *r = of_env(new environment(to_env_ref(e).add_universe(to_name_ref(u)))); + *r = of_env(new environment(module::add_universe(to_env_ref(e), to_name_ref(u)))); LEAN_CATCH; } @@ -37,7 +38,7 @@ lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exceptio LEAN_TRY; check_nonnull(e); check_nonnull(d); - *r = of_env(new environment(to_env_ref(e).add(to_cert_decl_ref(d)))); + *r = of_env(new environment(module::add(to_env_ref(e), to_cert_decl_ref(d)))); LEAN_CATCH; }