aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-03 13:37:41 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-03 13:37:41 +0200
commit3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (patch)
tree7a95c75037ddc1c729bc496c13084d350f9f29a1 /doc/refman
parent4bff930da2c029a66eaf5378e5abd2cc35554f8f (diff)
parent15d415729962eddde2cd1d58e03449c8526ba626 (diff)
Merge PR#411: Mention template polymorphism in the documentation.
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/RefMan-cic.tex12
-rw-r--r--doc/refman/RefMan-pre.tex2
2 files changed, 9 insertions, 5 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b9c17d814..fdd272581 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified
identifier with a number) or a successor of an algebraic universe (an
expression $u+1$), or an upper bound of algebraic universes (an
expression $max(u_1,...,u_n)$), or the base universe (the expression
-$0$) which corresponds, in the arity of sort-polymorphic inductive
-types (see Section \ref{Sort-polymorphism-inductive}),
+$0$) which corresponds, in the arity of template polymorphic inductive
+types (see Section \ref{Template-polymorphism}),
to the predicative sort {\Set}. A graph of constraints between
the universe variables is maintained globally. To ensure the existence
of a mapping of the universes to the positive integers, the graph of
@@ -977,8 +977,8 @@ Inductive exType (P:Type->Prop) : Type :=
%is recursive or not. We shall write the type $(x:_R T)C$ if it is
%a recursive argument and $(x:_P T)C$ if the argument is not recursive.
-\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}}
-\label{Sort-polymorphism-inductive}
+\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}}
+\label{Template-polymorphism}
Inductive types declared in {\Type} are
polymorphic over their arguments in {\Type}.
@@ -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
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f36969e82..0441f952d 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -529,7 +529,7 @@ intensive computations.
Christine Paulin implemented an extension of inductive types allowing
recursively non uniform parameters. Hugo Herbelin implemented
-sort-polymorphism for inductive types.
+sort-polymorphism for inductive types (now called template polymorphism).
Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary
compatible equivalence relations. He also generalized rewriting to