Leonardo de Moura
e80765daca
fix(library/export_decl): bug at export_decl_modification::perform
...
The `perform` method was adding the modification to the environment
where it was being applied.
2018-05-31 09:16:46 -07:00
Leonardo de Moura
75c63ec921
refactor(*): list<name> ==> obj_list<name>
2018-05-23 15:48:43 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07:00
Gabriel Ebner
a26e2c9108
feat(library/module): intermediary data structure for environment modifications
2016-12-20 10:15:19 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Sebastian Ullrich
e69b508492
refactor(library/export_decl): Re-implement for new scoped_ext
...
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
2016-07-29 23:44:22 -04:00
Sebastian Ullrich
c4edad0372
feat(frontends/lean, library): remove attribute and metaclass scoping
...
All data is now part of either a global, permanent scope or a local,
temporary one
2016-07-29 23:44:21 -04:00
Leonardo de Moura
224203f215
feat(library,frontends/lean/builtin_cmds): store export cmds and replay them
...
see #603
closes #723
2016-06-03 12:51:12 -07:00
