Proof-checking code; numerous fixups of segfaults and missing functionality in proof generation; fix bug 285.