diff options
| author | Pierre-Marie Pédrot | 2019-11-01 12:19:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 12:22:04 +0100 |
| commit | c5ce7dfe595beaced11646e3aed7e3532a1353f0 (patch) | |
| tree | bb89e15ab7e155918bce7588d593d163f05723ae /doc/changelog | |
| parent | 020cbc9ef9b2d4b22ee6e8490c59f63f87c25a25 (diff) | |
Add warnings regarding the experimental nature of the vos feature in the doc.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/08-tools/08642-vos-files.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst index 24a610c56b..f612096880 100644 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -1,7 +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 + 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). |