diff options
| author | SimonBoulier | 2018-11-15 12:12:58 +0100 |
|---|---|---|
| committer | SimonBoulier | 2019-08-16 11:43:51 +0200 |
| commit | de02e40124e4938fd4796303b8f5686e542fcb1a (patch) | |
| tree | 4a081e565bbc55a3bd1ca42fa783a43c65cfef8a /doc/sphinx/language | |
| parent | 6414a2a96f6d9a237baf08b7b449a55ee5d34376 (diff) | |
Add documentation for typing flags.
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. |