Vericert 1.2.2

Mainly fix some documentation and remove any Admitted theorems, even though
these were in parts of the compiler that were never used.