michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): rename method

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-29 11:46:27 -07:00
parent d1cb0018c0
commit 91abba3c3d
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/type_checker.cpp
View file

@ -354,7 +354,7 @@ pair<expr, constraint_seq> type_checker::check(expr const & e, level_param_names
return infer_type_core(e, false);
}
pair<expr, constraint_seq> type_checker::check_ignore_levels(expr const & e) {
pair<expr, constraint_seq> type_checker::check_ignore_undefined_universes(expr const & e) {
flet<level_param_names const *> updt(m_params, nullptr);
return infer_type_core(e, false);
}

4
src/kernel/type_checker.h
View file

@ -148,8 +148,8 @@ public:
The result is meaningful only if the generated constraints can be solved.
*/
pair<expr, constraint_seq> check(expr const & t, level_param_names const & ps = level_param_names());
/** \brief Like \c check, but ignores undefined universe level parameters */
pair<expr, constraint_seq> check_ignore_levels(expr const & e);
/** \brief Like \c check, but ignores undefined universes */
pair<expr, constraint_seq> check_ignore_undefined_universes(expr const & e);
/** \brief Return true iff t is definitionally equal to s. */
pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);

2
src/library/tactic/generalize_tactic.cpp
View file

@ -39,7 +39,7 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
expr new_t = mk_pi(n, e_t, abstract(t, *new_e));
expr new_m = g.mk_meta(ngen.next(), new_t);
try {
tc->check_ignore_levels(g.abstract(new_t));
tc->check_ignore_undefined_universes(g.abstract(new_t));
} catch (kernel_exception const & ex) {
std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {