From 539c31fe5a062bc9afce464155da44642a21e31e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Mar 2016 15:01:29 -0700 Subject: [PATCH] refactor(library/definitional): use new type_checker --- src/library/definitional/brec_on.cpp | 8 ++++---- src/library/definitional/cases_on.cpp | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 4413e6f7f8..52662afa31 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -44,7 +44,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow if (is_inductive_predicate(env, n)) return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); - old_type_checker tc(env); + type_checker tc(env); unsigned nparams = std::get<1>(decls); declaration ind_decl = env.get(n); declaration rec_decl = env.get(inductive::get_elim_name(n)); @@ -52,7 +52,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow unsigned nminors = *inductive::get_num_minor_premises(env, n); unsigned ntypeformers = length(std::get<2>(decls)); level_param_names lps = rec_decl.get_univ_params(); - bool is_reflexive = is_reflexive_datatype(tc.get_type_context(), n); + bool is_reflexive = is_reflexive_datatype(tc, n); level lvl = mk_param_univ(head(lps)); levels lvls = param_names_to_levels(tail(lps)); level_param_names blvls; // universe level parameters of ibelow/below @@ -167,7 +167,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) if (is_inductive_predicate(env, n)) return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); - old_type_checker tc(env); + type_checker tc(env); unsigned nparams = std::get<1>(decls); declaration ind_decl = env.get(n); declaration rec_decl = env.get(inductive::get_elim_name(n)); @@ -176,7 +176,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) unsigned nminors = *inductive::get_num_minor_premises(env, n); unsigned ntypeformers = length(std::get<2>(decls)); level_param_names lps = rec_decl.get_univ_params(); - bool is_reflexive = is_reflexive_datatype(tc.get_type_context(), n); + bool is_reflexive = is_reflexive_datatype(tc, n); level lvl = mk_param_univ(head(lps)); levels lvls = param_names_to_levels(tail(lps)); level rlvl; diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 5e2837ea1a..2f40e2b7d4 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/inductive/inductive.h" -#include "kernel/type_checker.h" #include "library/module.h" #include "library/protected.h" #include "library/reducible.h"