diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 91dfa34494..2cbd41af8b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -778,7 +778,8 @@ Simple inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. + the inductive definition. The positivity checking can be disabled using + the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. |