From effefb8b03ce7a3bdb2e5dae5beae0077a8b75e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jun 2018 12:16:51 -0700 Subject: [PATCH] chore(kernel/inductive): style --- src/kernel/inductive.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index f9da86bdb2..5398d58af2 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -111,10 +111,9 @@ public: } } - void check_constructor(constructor const & cnstr, unsigned decl_idx) { + void check_constructor(constructor const & cnstr, unsigned /* decl_idx */) { check_no_metavar_no_fvar(m_env, cnstr.m_name, cnstr.m_type); type_checker(m_env).check(cnstr.m_type, m_level_params); - } void check_constructors() { @@ -135,7 +134,7 @@ public: }; environment environment::add_inductive_decls(inductive_decls const & decls) const { - return add_inductive_fn(*this,decls)(); + return add_inductive_fn(*this, decls)(); } void initialize_inductive() {