# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1548014432 18000
# Node ID ec0ce5129fc46bfd9b5fc707fd66d2f86b8458e7
# Parent  1a231194d164151afe91cfa593dbacdf73288764
Switch to new approach to supporting newer Coq versions while still building with patched Coq 8.4

diff -r 1a231194d164 -r ec0ce5129fc4 src/StackMachine.v
--- 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.