Leonardo de Moura
|
98aefca014
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
Leonardo de Moura
|
04fe48539f
|
feat(library/tactic/revert_tactic): low level version of 'revert' tactic
|
2016-07-14 14:42:56 -04:00 |
|
Leonardo de Moura
|
f1986b57e9
|
feat(library/init/meta/tactic): 'revert' tactic returns the number of actually reverted hypothesis
|
2016-06-28 15:36:50 +01:00 |
|
Leonardo de Moura
|
59f2b9e8c2
|
refactor(library/type_context): "metavar_context & m_mctx" ==> "metavar_context m_mctx"
|
2016-06-25 13:08:03 -07:00 |
|
Leonardo de Moura
|
a29e1b76d3
|
refactor(library/tactic/revert_tactic): revert take a local instead of a name
|
2016-06-22 15:20:02 -07:00 |
|
Leonardo de Moura
|
195512e125
|
fix(library/type_context, library/tactic/revert_tactic): result must contain also reverted let-decls
|
2016-06-21 16:32:02 -07:00 |
|
Leonardo de Moura
|
a136c2ec1e
|
fix(library/tactic/revert_tactic): update output parameter
|
2016-06-14 17:56:12 -07:00 |
|
Leonardo de Moura
|
9bcb4e05db
|
feat(library/tactic): store tactic_state at failure
|
2016-06-13 15:25:55 -07:00 |
|
Leonardo de Moura
|
290a925c5f
|
fix(library/tactic/revert_tactic): type_context revert method already assigns metavar
|
2016-06-13 12:53:56 -07:00 |
|
Leonardo de Moura
|
62116f5b4b
|
feat(library/tactic): add 'revert' tactic
|
2016-06-11 10:12:43 -07:00 |
|
Leonardo de Moura
|
aeee79da2b
|
chore(library): library/tactic => library/old_tactic
|
2016-06-06 16:38:27 -07:00 |
|
Leonardo de Moura
|
d8079aa16a
|
refactor(library): create copy of the kernel type_checker in library
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
|
2016-03-18 14:34:10 -07:00 |
|
Leonardo de Moura
|
c9e9fee76a
|
refactor(*): remove name_generator and use simpler mk_fresh_name
|
2016-02-11 18:05:57 -08:00 |
|
Leonardo de Moura
|
3912bc24c8
|
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
|
2015-04-30 11:00:39 -07:00 |
|
Leonardo de Moura
|
4ea323a2b2
|
refactor(library/tactic): cleanup common pattern
|
2015-03-12 14:52:41 -07:00 |
|
Leonardo de Moura
|
368f9d347e
|
refactor(frontends/lean): approach used to parse tactics
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
|
2015-03-05 18:11:21 -08:00 |
|
Leonardo de Moura
|
7fc216183e
|
feat(library/tactic): produce better error message when a tactic fails
closes #348
|
2015-02-16 18:42:15 -08:00 |
|
Leonardo de Moura
|
27f6bfd3f0
|
refactor(*): add file constants.txt with all constants used by the Lean binary
|
2015-01-23 16:50:32 -08:00 |
|
Leonardo de Moura
|
2a00647089
|
refactor(library/tactic): cleanup 'revert' and 'clear' tactics
|
2014-11-26 17:08:14 -08:00 |
|
Leonardo de Moura
|
e55397d422
|
feat(library/tactic): add 'clears' and 'reverts' variants
|
2014-11-26 14:49:48 -08:00 |
|
Leonardo de Moura
|
2bd8f969d5
|
feat(library/tactic): add 'revert' tactic, closes #346
|
2014-11-26 14:23:42 -08:00 |
|