From 5cf8ec5afe59a420130a6b0828e48b6d87bb1e3c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 11:51:28 +0200
Subject: Add doc for template polymorphism option and attributes.

---
 doc/sphinx/language/cic.rst | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 3d3a1b11b1..35f45e2e0e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1025,8 +1025,26 @@ the Type hierarchy.
 Template polymorphism
 +++++++++++++++++++++
 
-Inductive types declared in :math:`\Type` are polymorphic over their arguments
-in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
+Inductive types can be made polymorphic over their arguments
+in :math:`\Type`.
+
+.. opt:: Auto Template Polymorphism
+
+  This option, enabled by default, makes every inductive type declared
+  at level :math:`Type` (without annotations or hiding it behind a
+  definition) template polymorphic.
+
+  This can be prevented using the ``notemplate`` attribute.
+
+  An inductive type can be forced to be template polymorphic using the
+  ``template`` attribute.
+
+  Template polymorphism and universe polymorphism (see Chapter
+  :ref:`polymorphicuniverses`) are incompatible, so if the later is
+  enabled it will prevail over automatic template polymorphism and
+  cause an error when using the ``template`` attribute.
+
+If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
 Especially, if :math:`A` is well-typed in some global environment and local
 context, then :math:`A_{/s}` is typable by typability of all products in the
-- 
cgit v1.2.3