From 41b3486501f0217f0b0c552f21d6f0374b55a3ba Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Sat, 28 Jan 2017 14:02:02 +0100
Subject: Mention template polymorphism in the documentation.

Since About mentions it the doc should as well.
---
 doc/refman/RefMan-cic.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b9c17d814..12f390e44 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1120,6 +1120,12 @@ Check (fun (A:Prop) (B:Set) => prod A B).
 Check (fun (A:Type) (B:Prop) => prod A B).
 \end{coq_example}
 
+Internally, Coq calls sort polymorphism of inductive types
+{\em template polymorphism}. For instance:
+\begin{coq_example}
+About prod.
+\end{coq_example}
+
 \subsection{Destructors}
 The specification of inductive definitions with arities and
 constructors is quite natural.  But we still have to say how to use an
-- 
cgit v1.2.3