From 15d415729962eddde2cd1d58e03449c8526ba626 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 24 Apr 2017 16:39:25 +0200
Subject: refman: remember the old name of template polymorphism.

---
 doc/refman/RefMan-cic.tex | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e26d4b18da..fdd2725810 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1120,6 +1120,10 @@ Check (fun (A:Prop) (B:Set) => prod A B).
 Check (fun (A:Type) (B:Prop) => prod A B).
 \end{coq_example}
 
+\Rem Template polymorphism used to be called ``sort-polymorphism of
+inductive types'' before universe polymorphism (see
+Chapter~\ref{Universes-full}) was introduced.
+
 \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