3 commits

Author	SHA1	Message	Date
Leonardo de Moura	eeb6c72508	feat(frontends/lean): modify begin-end semantics, closes #258	2014-10-28 22:15:38 -07:00
Leonardo de Moura	186e598bf8	feat(library/tactic/goal): add option pp.compact_goals	2014-10-28 16:30:37 -07:00
Leonardo de Moura	a544d32fcf	fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders	2014-10-26 16:11:58 -07:00