Leonardo de Moura
|
49d5af473d
|
refactor(kernel): remove support for proof irrelevant classes
Motivation: we can use Prop
|
2014-09-19 07:32:07 -07:00 |
|
Leonardo de Moura
|
7df78ea503
|
feat(kernel): add combinator for combining normalizer_extensions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 10:00:40 -07:00 |
|
Leonardo de Moura
|
72bce91c18
|
refactor(library/unifier): move inductive datatype support to inductive_unifier_plugin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-05 11:00:35 -07:00 |
|
Leonardo de Moura
|
e445515f2b
|
refactor(kernel): move standard and hott kernel instantiations to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-05 10:31:27 -07:00 |
|