Add warnings regarding the experimental nature of the vos feature in the doc.

2 files changed, 3 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).
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.**