chore(kernel/inductive): style

leanprover · Jun 12, 2018 · effefb8 · effefb8
1 parent e9b4b81
commit effefb8
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
@@ -111,10 +111,9 @@ class add_inductive_fn {
         }
     }
 
-    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 @@ class add_inductive_fn {
 };
 
 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() {