Mercurial > cpdt > repo
comparison src/StackMachine.v @ 563:af97676583f3
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 07 Jan 2018 11:53:31 -0500 |
| parents | d65e9c1c9041 |
| children | ec0ce5129fc4 |
comparison
equal
deleted
inserted
replaced
| 562:36b1f893c1e0 | 563:af97676583f3 |
|---|---|
| 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. For instance, we run a command to output the OCaml version of [tcompile]:%\index{Vernacular commands!Extraction}% *) |
| 852 | 852 |
| 853 Require Extraction. | |
| 853 Extraction tcompile. | 854 Extraction tcompile. |
| 854 | 855 |
| 855 (** << | 856 (** << |
| 856 let rec tcompile t e ts = | 857 let rec tcompile t e ts = |
| 857 match e with | 858 match e with |