Mercurial > cpdt > repo

diff src/StackMachine.v @ 563:af97676583f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -0500
parents d65e9c1c9041
children ec0ce5129fc4
line wrap: on
line diff
--- a/src/StackMachine.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/StackMachine.v	Sun Jan 07 11:53:31 2018 -0500
@@ -850,6 +850,7 @@
 
 (** It is probably worth emphasizing that we are doing more than building mathematical models.  Our compilers are functional programs that can be executed efficiently.  One strategy for doing so is based on%\index{program extraction}% _program extraction_, which generates OCaml code from Coq developments.  For instance, we run a command to output the OCaml version of [tcompile]:%\index{Vernacular commands!Extraction}% *)
 
+Require Extraction.
 Extraction tcompile.
 
 (** <<