In the Kami project, that causes a stack overflow in one of the example files

(ProcThreeStInl.v, when the final "Defined" runs). I've verified that the
change here fixes the stack overflow there with Coq 8.5pl2.

In this version, all the recursive calls are in tail position. Instead of
taking a single list of instructions, `emit' here takes a curent list and a remaining
list of lists of instructions. That means the two calls elsewhere in the file now
add an empty list argument. The algorithm works on the current list until it's empty,
then works on the remaining lists. The most complex case is for Ksequence, where
one of the pieces becomes the new current list, and the other pieces are consed onto
the remaining sub-lists.

0 files changed, 0 insertions, 0 deletions