max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/kernel
History
Leonardo de Moura 173eb1c6b7 refactor(util/fresh_name): implement fresh_name using unique thread id 
@kha This commit is retracting the experiment using
`mk_fresh_name_generator_child` when creating new tasks.
The names get too long.

I'm still refactoring the code and trying to eliminate all occurrences
of `mk_fresh_name`. I still have a long way to go, but I am merging
this branch into master since it has many other fixes.
2018-02-23 10:35:04 -08:00
..
inductive feat(util/name_generator): name generator prefix bookkeeping 2018-02-21 15:04:19 -08:00
quotient chore(kernel/quotient/quotient): update comments 2017-03-07 14:11:51 -08:00
abstract.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
abstract.h fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls 2017-04-26 14:22:36 -07:00
abstract_type_context.cpp refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name 2018-02-21 15:04:19 -08:00
abstract_type_context.h refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name 2018-02-21 15:04:19 -08:00
cache_stack.h
CMakeLists.txt refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
declaration.cpp fix(library/tactic/simp_lemmas): auto_params when adding simp lemmas 2017-12-09 09:47:39 -08:00
declaration.h refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.h chore(kernel/environment): rename method 2017-05-15 14:18:16 -07:00
equiv_manager.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
equiv_manager.h feat(kernel/equiv_manager): use expr_struct_map in the equiv_manager 2016-07-07 07:39:25 -07:00
error_msgs.cpp feat(src/kernel/error_msgs): show aliased variables when printing error messages 2017-09-05 16:46:44 -07:00
error_msgs.h feat(frontends/lean/elaborator): closes #1760 2017-08-21 16:15:03 -07:00
expr.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
expr.h feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr_cache.cpp
expr_cache.h
expr_eq_fn.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
expr_eq_fn.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_maps.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_pair.h feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
expr_sets.h
ext_exception.h chore(util,kernel,library): clang warnings 2017-02-17 20:01:34 -08:00
find_fn.h
for_each_fn.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
for_each_fn.h
formatter.cpp
formatter.h feat(library/type_context): better error messages 2016-09-28 15:59:43 -07:00
free_vars.cpp feat(kernel): add compilation flag for disabling "free var range" optimization 2017-02-21 19:40:56 -08:00
free_vars.h
init_module.cpp fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
init_module.h
instantiate.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
instantiate.h feat(kernel/instantiate): add helper function 2016-08-14 16:16:03 -07:00
kernel_exception.cpp feat(frontends/lean/elaborator): closes #1760 2017-08-21 16:15:03 -07:00
kernel_exception.h fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error 2017-03-27 13:42:08 -07:00
level.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
level.h feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
normalizer_extension.cpp feat(msvc): further work on MSVC compatibility 2018-02-06 10:11:09 -08:00
normalizer_extension.h feat(msvc): further work on MSVC compatibility 2018-02-06 10:11:09 -08:00
pos_info_provider.cpp
pos_info_provider.h feat(kernel/pos_info_provider): add save_pos_info 2017-03-31 09:40:48 -07:00
replace_fn.cpp chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
replace_fn.h
scope_pos_info_provider.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
scope_pos_info_provider.h refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
standard_kernel.cpp feat(msvc): further work on MSVC compatibility 2018-02-06 10:11:09 -08:00
standard_kernel.h refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
type_checker.cpp feat(util/name_generator): name generator prefix bookkeeping 2018-02-21 15:04:19 -08:00
type_checker.h refactor(util/fresh_name): implement fresh_name using unique thread id 2018-02-23 10:35:04 -08:00