A word to the wise: use my fork of Coq to avoid annoying syntax errors in extraction. Not strictly necessary (you can fix the errors manually or with a script without much trouble), but quite a bit less vexing.
jonsterling / coq-up Goto Github PK
View Code? Open in Web Editor NEWA tarpit in Coq