Leonardo de Moura
|
81a694e73c
|
chore(frontends/lean): remove dead code
|
2018-09-08 15:44:49 -07:00 |
|
Leonardo de Moura
|
fabfe32ca5
|
chore(*): remove unnecessary scoped_ext dependencies
|
2018-09-08 15:42:48 -07:00 |
|
Leonardo de Moura
|
5d00936a8f
|
chore(*): remove some old_type_checker dependencies
|
2018-09-07 08:48:21 -07:00 |
|
Leonardo de Moura
|
58e91559d0
|
feat(*): use new inductive datatype module
|
2018-09-06 18:09:22 -07:00 |
|
Leonardo de Moura
|
1dfcea58f9
|
chore(*): remove some references to old inductive datatype module
|
2018-09-04 10:45:17 -07:00 |
|
Leonardo de Moura
|
dd03747d22
|
chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies
|
2018-09-03 13:05:42 -07:00 |
|
Sebastian Ullrich
|
39cdae50ee
|
feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms
|
2018-09-02 18:08:41 -07:00 |
|
Sebastian Ullrich
|
3bdc0db397
|
feat(library/derive_attribute): allow implicit parameters in class signature
|
2018-08-29 16:42:24 -07:00 |
|
Sebastian Ullrich
|
f4a9798f9b
|
fix(library/derive_attribute): avoid segfault on sorry input
|
2018-08-29 16:42:24 -07:00 |
|
Sebastian Ullrich
|
5c066b6e84
|
fix(library/derive_attribute): pass options to type_context
|
2018-08-23 10:48:38 -07:00 |
|
Leonardo de Moura
|
f3e99286bb
|
chore(kernel): remove certified_declaration
|
2018-08-22 12:11:34 -07:00 |
|
Sebastian Ullrich
|
d4364850ff
|
feat(library/derive_attribute): support out_params after main parameter
|
2018-08-02 14:45:37 -07:00 |
|
Sebastian Ullrich
|
10adf10634
|
fix(library/derive_attribute): prevent infinite loop during parsing
|
2018-08-02 08:08:21 -07:00 |
|
Sebastian Ullrich
|
eda9e4bb3f
|
feat(library/derive_attribute): temporary, hacky C++ implementation of @[derive]
|
2018-08-01 18:44:23 -07:00 |
|