Mercurial > cpdt > repo
comparison src/StackMachine.v @ 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 | 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 (** << |