3 commits

Author	SHA1	Message	Date
Leonardo de Moura	cd6acb5d1d	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07:00
Leonardo de Moura	aa2f9fadee	feat(frontends/lean/elaborator): add support for nondependent eliminators in the new elaborator	2016-09-12 15:26:13 -07:00
Leonardo de Moura	22b8cb2777	fix(library/type_context): whnf cache bug	2016-08-18 18:04:19 -07:00