From de02e40124e4938fd4796303b8f5686e542fcb1a Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 15 Nov 2018 12:12:58 +0100
Subject: Add documentation for typing flags.

---
 doc/sphinx/language/gallina-specification-language.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/language')

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.
 
-- 
cgit v1.2.3