From 41b3486501f0217f0b0c552f21d6f0374b55a3ba Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert 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 From d3a2acc9fceff7476bc2d9eaadab8411365172a2 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 31 Mar 2017 15:03:34 +0200 Subject: Use "template polymorphism" in the documentation. --- doc/refman/RefMan-cic.tex | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 12f390e44..e26d4b18d 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,12 +1120,6 @@ 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 From d70af8a387d1199be3327b3e4ef21dda9bb2155e Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 11 Apr 2017 12:47:29 +0200 Subject: Update RefMan-pre to mention template polymorphism. --- doc/refman/RefMan-pre.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') 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 -- cgit v1.2.3 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(+) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e26d4b18d..fdd272581 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