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/sphinx/practical-tools/coq-commands.rst | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx')

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