Mercurial > cpdt > repo
changeset 567:ec0ce5129fc4
Switch to new approach to supporting newer Coq versions while still building with patched Coq 8.4
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2019 15:00:32 -0500 |
| parents | 1a231194d164 |
| children | 81d63d9c1cc5 |
| files | src/StackMachine.v |
| diffstat | 1 files changed, 5 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/StackMachine.v Fri Oct 19 10:27:35 2018 -0400 +++ b/src/StackMachine.v Sun Jan 20 15:00:32 2019 -0500 @@ -848,7 +848,11 @@ Qed. (* end thide *) -(** 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}% *) +(** 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. + + To set up the feature properly in recent versions of Coq, we must run the command [Require Extraction.]. However, this book %PDF%#HTML# is still built with a patched old version of Coq that neither requires nor allows that command, so it is commented out in this rendering! + + Now we run a command to output the OCaml version of [tcompile]:%\index{Vernacular commands!Extraction}% *) Require Extraction. Extraction tcompile.