Leonardo de Moura
|
a64d1a77ea
|
refactor(library, frontends/lean): remove old coercion management module
|
2016-07-29 13:51:26 -07:00 |
|
Leonardo de Moura
|
7a92ce38bd
|
refactor(frontends/lean): elaborator_exception ==> old_elaborator_exception
|
2016-07-26 16:24:28 -07:00 |
|
Leonardo de Moura
|
90d920b7c9
|
chore(frontends/lean,library/explicit): remove dead code
|
2016-07-02 01:57:43 +01:00 |
|
Leonardo de Moura
|
1a5756661f
|
refactor(frontends/lean,library): move scope_pos_info_provider to library
|
2016-06-30 10:19:35 +01:00 |
|
Leonardo de Moura
|
bb70fbbd48
|
refactor(frontends/lean): simplify elaborator_context
|
2016-06-29 16:56:19 +01:00 |
|
Leonardo de Moura
|
ccc65c6171
|
refactor(frontends/lean): add thread local parser_pos_provider
|
2016-06-29 16:09:06 +01:00 |
|
Leonardo de Moura
|
f3803c6ee4
|
refactor(frontends/lean/elaborator_context): remove io_state from elaborator_context
|
2016-06-27 06:29:54 +01:00 |
|
Leonardo de Moura
|
2b35b0056a
|
chore(library/metavar_closure): remove dead code
|
2016-06-25 13:29:59 -07: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
|
d604cb8b4e
|
feat(library/vm/vm): add friendly invoke method
|
2016-06-24 15:49:40 -07:00 |
|
Leonardo de Moura
|
2b43f591c9
|
fix(library/type_context): remove m_cache_owner field
This idiom creates problem if we use (even accidentally) the copy constructor.
|
2016-06-23 14:03:46 -07:00 |
|
Leonardo de Moura
|
35888fae2c
|
refactor(util/list): remove coercion from T -> list<T>
|
2016-06-22 10:00:07 -07:00 |
|
Leonardo de Moura
|
0261cb95bf
|
feat(frontends/lean/old_elaborator): use type_context for failure tactic_state
|
2016-06-20 11:09:14 -07:00 |
|
Leonardo de Moura
|
0eb42190f0
|
fix(tests/lean): tests
|
2016-06-14 21:52:52 -07:00 |
|
Leonardo de Moura
|
6a22c0f771
|
chore(frontends/lean/old_elaborator): improve error message
|
2016-06-14 21:47:29 -07:00 |
|
Daniel Selsam
|
214e960574
|
fix(frontends/lean/elaborator): incorrect assertion
Conflicts:
src/frontends/lean/elaborator.cpp
|
2016-06-14 18:05:39 -07:00 |
|
Leonardo de Moura
|
26c10c368a
|
refactor(library): instantiate ==> instantiate_mvars
Motivation: avoid confusion with 'instantiate' procedure for variables
|
2016-06-14 10:29:47 -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
|
6d78d0cc98
|
feat(frontends/lean/old_elaborator): interface old_elaborator with new tactic framework
The interface is not efficient, but it is sufficient for testing
purposes. We will replace the elaborator with a new one.
|
2016-06-13 13:59:01 -07:00 |
|
Leonardo de Moura
|
5382a5a556
|
feat(frontends/lean): allow unbounded recursion in meta_definitions
|
2016-06-01 09:55:07 -07:00 |
|
Leonardo de Moura
|
fdea718d9d
|
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
|
2016-04-25 15:41:12 -07:00 |
|
Leonardo de Moura
|
d88098f38d
|
chore(frontends/lean): remove some of the tactic support
|
2016-04-25 15:26:56 -07:00 |
|
Leonardo de Moura
|
03809e7973
|
refactor(frontends/lean): elaborator_context
|
2016-04-05 16:19:06 -07:00 |
|
Leonardo de Moura
|
2577be6344
|
chore(frontends/lean): remove useless elaborator options
|
2016-04-05 16:03:10 -07:00 |
|
Leonardo de Moura
|
75549bafd7
|
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
|
2016-03-30 14:59:18 -07:00 |
|