6 commits

Author	SHA1	Message	Date
Leonardo de Moura	a796bda14e	refactor(library/tactic): use new simp_lemmas module in the simplifier	2016-10-08 21:54:34 -07:00
Leonardo de Moura	3fbdb71f3e	feat(library/tactic/simplifier): remove simp_extensions	2016-10-06 20:50:23 -07:00
Leonardo de Moura	d747fcb17c	refactor(library/tactic/simp_lemmas): new caching mechanism	2016-10-06 20:20:01 -07:00
Leonardo de Moura	572751c56e	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class ... Before this commit, we were inferring whether an inductive/structure/class were meta or not. This was bad since the user had no clue whether the type was trusted (non meta) or not. Moreover, users could get confused by this behavior and assume the kernel was allowing trusted code to rely on untrusted one.	2016-09-29 17:56:35 -07:00
Daniel Selsam	52f87760d8	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
Daniel Selsam	b0c5744eea	feat(inductive_compiler): support for mutually inductive types	2016-09-10 14:22:27 -07:00