Leonardo de Moura 607d22ae58 fix(library/compiler/csimp): bug at float_cases_on_core ... The bug occurs when floating `cases_on` application in code of the form ``` let x := C.cases_on ... in t ``` and when the type of `t` depends on `x`. The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it. We fix the bug by replacing `x` with its value in the type. cc @kha		2018-11-30 11:40:41 -08:00
..
ir	feat(library/init/lean/ir): remove support for functions with multiple return values	2018-10-22 17:39:40 -07:00
parser	feat(library/init/lean/expander): preresolve global references (not actually used anywhere yet)	2018-11-27 18:02:51 +01:00
config.lean	feat(library/init/lean): add lean.closure_max_args	2018-05-13 08:40:46 -07:00
declaration.lean	feat(kernel): save constructor idx and nfields at constructor_val	2018-09-14 13:45:58 -07:00
disjoint_set.lean	feat(library/init/lean/ir): add elim_phi function	2018-05-06 10:07:44 -07:00
elaborator.lean	fix(library/compiler/csimp): bug at float_cases_on_core	2018-11-30 11:40:41 -08:00
expander.lean	feat(library/init/lean/expander): preresolve global references (not actually used anywhere yet)	2018-11-27 18:02:51 +01:00
expr.lean	feat(kernel): store structure name in proj-expressions	2018-10-02 09:23:11 -07:00
format.lean	refactor(frontends/lean/elaborator): mark thunk as opaque, and thunk A to A is now a coercion	2018-08-21 15:27:51 -07:00
kvmap.lean	feat(library/init/lean): add kvmap	2018-06-15 16:05:11 -07:00
level.lean	feat(library/init/lean/level): missing functions	2018-05-22 10:49:24 -07:00
message.lean	fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end	2018-09-11 13:55:25 -07:00
name.lean	feat(library/init/data): annotate rbtree and rbmap functions	2018-10-19 14:57:31 -07:00
name_mangling.lean	chore(library): remove >>, we should use *>	2018-09-12 17:31:21 -07:00
options.lean	feat(library/init/lean): add kvmap	2018-06-15 16:05:11 -07:00
pos.lean	feat(library/init/core): decidable_eq is a proper class	2018-09-07 16:38:11 -07:00
trace.lean	refactor(frontends/lean/elaborator): mark thunk as opaque, and thunk A to A is now a coercion	2018-08-21 15:27:51 -07:00