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.