diff options
| author | Maxime Dénès | 2019-10-23 15:10:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 12:16:48 +0100 |
| commit | fb6afb4a7256b33725660668738bc17c84ae94f5 (patch) | |
| tree | 2f3e3aa6bf1b23d61fc8c26405a0df13be5df1a3 | |
| parent | a779415f6c39cebcb0384dec0673cde71c05e3b2 (diff) | |
Changelog entry
| -rw-r--r-- | doc/changelog/08-tools/08642-vos-files.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst new file mode 100644 index 0000000000..24a610c56b --- /dev/null +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -0,0 +1,7 @@ +- `coqc` now provides the ability to generate compiled interfaces. + Use `coqc -vos foo.v` to skip all opaque proofs during the + compilation of `foo.v`, and output a file called `foo.vos`. + This feature enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). |