From 55b8347e758e86ca34aafaa635d48492c812bc3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 7 Jan 2019 13:06:21 +0100
Subject: Add doc for auto-template warning

---
 doc/sphinx/language/cic.rst | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index cc5d9d6205..693ee28a47 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1041,6 +1041,12 @@ in :math:`\Type`.
    enabled it will prevail over automatic template polymorphism and
    cause an error when using the ``template`` attribute.
 
+.. warn:: Automatically declaring @ident as template polymorphic.
+
+   Warning ``auto-template`` can be used to find which types are
+   implicitly declared template polymorphic by :flag:`Auto Template
+   Polymorphism`.
+
 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
-- 
cgit v1.2.3