3 commits

Author	SHA1	Message	Date
Sebastian Ullrich	2185ee7e95	feat(library/tactic): make let tactic transparent, introduce new opaque note tactic ... The new let tactic is semantically equivalent to let terms, while `note` preserves its old opaque behavior.	2015-12-14 10:14:02 -08:00
Leonardo de Moura	b6bac2e542	chore(tests/lean/run): adjust tests	2015-12-13 12:23:44 -08:00
Leonardo de Moura	68688ecdf6	fix(library/tactic/subst_tactic): in the standard mode, use dependent elimination in the subst tactic (when needed) ... Before this commit, the subst tactic was producing an type incorrect result when dependent elimination was needed (see new test for an example).	2015-06-03 17:36:04 -07:00