7 commits

Author	SHA1	Message	Date
Leonardo de Moura	82095cc018	refactor(kernel): split declaration into declaration and constant_info ... This is just another step towards the design described at commit 16598391a07d4a	2018-08-22 17:53:11 -07:00
Leonardo de Moura	ec1aa2553c	refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object ... TODO: inductive, constructor, recursor	2018-06-25 10:05:45 -07:00
Leonardo de Moura	ce0467638e	chore(*): remove unification hints	2018-04-10 16:29:04 -07:00
Leonardo de Moura	bdea7d420d	chore(*): type_context ==> type_context_old	2018-03-05 12:38:24 -08:00
Leonardo de Moura	f873def910	refactor(library/type_context): move unification_hints to cache object	2018-03-05 12:17:09 -08:00
Leonardo de Moura	1aeaed0cae	feat(library/abstract_context_cache): make it fully abstract	2018-02-21 15:04:20 -08:00
Leonardo de Moura	a175e9393e	refactor(library): context_cache ==> abstract_context_cache	2018-02-21 15:04:20 -08:00

Renamed from src/library/context_cache.cpp (Browse further)