diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 |
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.** |