2 commits

Author	SHA1	Message	Date
Floris van Doorn	27cde0aeae	feat(hott): rename ppi_gen to ppi	2017-07-21 15:53:34 +01:00
Floris van Doorn	a02ea6b751	Unfold macros using the full typechecker in normalize. ... Fix #7. The problem (as I understand it) was that macros were expanded using a typechecker which didn't unfold (semireducible) definitions, which led to the macros not being unfolded correctly. Many many many thanks to @gebner!	2017-07-20 12:09:39 +01:00