HoTT/HoTT — pull request #303 by ezyang (2013-12-30 12:34:54+00:00)
Title: Split off HoTTBookExercises.v from HoTTBook.v.

Since exercise formalizations tend to be a lot wordier than mere
backreferences to theorems in the library (as discussed in PR #302),
this patch splits HoTTBook.v into a separate exercises file, which
contains formalizations for the exercises in the HoTT book. etc/Book.v
now takes a new flag, '--exercises', which instructs it to extract out
only exercises from the book; its default setting now no longer inserts
markers for exercises.

Signed-off-by: Edward Z. Yang