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

1 files changed, 2 insertions, 0 deletions

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.**