diff options
Diffstat (limited to 'doc/changelog/08-tools/08642-vos-files.rst')
| -rw-r--r-- | doc/changelog/08-tools/08642-vos-files.rst | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst deleted file mode 100644 index 83937390fc..0000000000 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Added:** - `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 is experimental. It 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). |