max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/module): has_sorry: check examples

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-24 14:46:47 +01:00
parent 43a7dd8e4f
commit 1182d8e7f7
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/module.cpp
View file

@ -388,6 +388,8 @@ environment update_module_defs(environment const & env, declaration const & d) {
static optional<name> should_report_sorry(name const & n) {
if (n.is_anonymous())
return optional<name>();
if (n == name{"_example"})
return optional<name>(n);
if (!is_internal_name(n))
return optional<name>(n);
if (!n.is_string() || n.is_atomic())