Mercurial > cpdt > repo

comparison src/StackMachine.v @ 567:ec0ce5129fc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 af97676583f3
children
comparison
equal deleted inserted replaced
566:1a231194d164 567:ec0ce5129fc4
846 tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 846 tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
847 crush. 847 crush.
848 Qed. 848 Qed.
849 (* end thide *) 849 (* end thide *)
850 850
851 (** 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}% *) 851 (** 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.
852
853 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!
854
855 Now we run a command to output the OCaml version of [tcompile]:%\index{Vernacular commands!Extraction}% *)
852 856
853 Require Extraction. 857 Require Extraction.
854 Extraction tcompile. 858 Extraction tcompile.
855 859
856 (** << 860 (** <<