Skip to content

Commit

Permalink
Update doc/sphinx/language/gallina-specification-language.rst
Browse files Browse the repository at this point in the history
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
  • Loading branch information
SimonBoulier and SkySkimmer committed Jun 4, 2019
1 parent 8152a47 commit 393d598
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/sphinx/language/gallina-specification-language.rst
Expand Up @@ -766,7 +766,7 @@ 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 positivity checking can be disabled using
the command :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`).
the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`).

.. exn:: The conclusion of @type is not valid; it must be built from @ident.

Expand Down

0 comments on commit 393d598

Please sign in to comment.