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

chore: show (first) declaration name with compilation times

Browse source
This commit is contained in:
Sebastian Ullrich 2021-06-16 15:39:01 +02:00
parent 389a274d45
commit 227a67cf8b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/compiler.cpp
View file

@ -187,7 +187,7 @@ environment compile(environment const & env, options const & opts, names cs) {
if (!cinfo.is_definition() && !cinfo.is_opaque()) return env;
}
time_task t("compilation", opts);
time_task t("compilation", opts, head(cs));
scope_trace_env scope_trace(env, opts);
comp_decls ds = to_comp_decls(env, cs);