Yeah. Sorry for stringing you along like this, but would it be too much to ask then to separate the exercises out into `contrib/HoTTBookExercises.v` or some such? Maybe we should have a subdirectory `contrib/HoTTBook`? Hmm, we would need to also process the exercise files, as in principle those could get renumbered or added. Ok, we need to think about this a bit.