From c5ce7dfe595beaced11646e3aed7e3532a1353f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Nov 2019 12:19:57 +0100 Subject: Add warnings regarding the experimental nature of the vos feature in the doc. --- doc/changelog/08-tools/08642-vos-files.rst | 2 +- doc/sphinx/practical-tools/coq-commands.rst | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) 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 `_ by Arthur Charguéraud, review by Maxime Dénès and Emilio Gallego). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d8325287cc..70259ff565 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -267,6 +267,8 @@ the proofs that it contains. At the end of the day, one still needs to proof check all files by producing standard ``.vo`` files. (Technically, when using ``-vos``, fewer universe constraints are collected.) + Moreover, this feature is still experimental, it may be subject to + change without prior notice. **Principle.** -- cgit v1.2.3