diff options
Diffstat (limited to 'doc/changelog/08-tools/08642-vos-files.rst')
| -rw-r--r-- | doc/changelog/08-tools/08642-vos-files.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst index f612096880..83937390fc 100644 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -1,4 +1,5 @@ -- `coqc` now provides the ability to generate compiled interfaces. +- **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 |