3 commits

Author	SHA1	Message	Date
Leonardo de Moura	83e4c0fcec	feat(frontends/lean): hide tactic "types" ... it is not very useful to display the type of tactics (e.g., apply, intros, ...)	2014-10-28 22:38:10 -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	e750c9b67a	feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode	2014-10-23 13:18:30 -07:00