Comment by tkz1312

I've been extracting a lot of verified C from theorem provers recently.