From 3958d8485a239836221e28cbf4dbed287ac3ea75 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Nov 2016 15:02:49 -0700 Subject: [PATCH] chore(library/module): remove dead code --- src/library/module.cpp | 7 ------- src/library/module.h | 13 ------------- 2 files changed, 20 deletions(-) diff --git a/src/library/module.cpp b/src/library/module.cpp index bdd164dafe..4b5d91b4a5 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -289,13 +289,6 @@ static void inductive_reader(deserializer & d, shared_environment & senv, return cdecl.add(env); }); } - -environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, - unsigned num_params, expr const & type, list const & intro_rules, - bool is_trusted) { - inductive::inductive_decl decl(ind_name, level_params, num_params, type, intro_rules); - return module::add_inductive(env, decl, is_trusted); -} } // end of namespace module struct import_modules_fn { diff --git a/src/library/module.h b/src/library/module.h index eba9d79813..47bd752e80 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -115,20 +115,7 @@ environment declare_quotient(environment const & env); /** \brief The following function must be invoked to register the builtin HITs in the kernel. */ environment declare_hits(environment const & env); - -/** - \brief Declare a single inductive datatype. This is just a helper function implemented on top of - the previous (more general) add_inductive. -*/ -environment add_inductive(environment const & env, - name const & ind_name, // name of new inductive datatype - level_param_names const & level_params, // level parameters - unsigned num_params, // number of params - expr const & type, // type of the form: params -> indices -> Type - list const & intro_rules); // introduction rules - } - void initialize_module(); void finalize_module(); }