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

feat(library/normalize): validate unfold-c hints

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-06 12:42:53 -08:00
parent 7205382f8c
commit ba641d7c58
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/normalize.cpp
View file

@ -64,6 +64,9 @@ template class scoped_ext<unfold_c_hint_config>;
typedef scoped_ext<unfold_c_hint_config> unfold_c_hint_ext;
environment add_unfold_c_hint(environment const & env, name const & n, optional<unsigned> idx, bool persistent) {
declaration const & d = env.get(n);
if (!d.is_definition() || d.is_opaque())
throw exception("invalid unfold-c hint, declaration must be a non-opaque definition");
return unfold_c_hint_ext::add_entry(env, get_dummy_ios(), unfold_c_hint_entry(n, idx), persistent);
}