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(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b9c17d8148..12f390e44f 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(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 12f390e44f..e26d4b18da 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 fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:46:23 +0200
Subject: Update various comments to use "template polymorphism"

Also remove obvious comments.
---
 checker/subtyping.ml                  | 2 +-
 checker/typeops.ml                    | 4 +---
 engine/universes.mli                  | 2 +-
 kernel/subtyping.ml                   | 2 +-
 kernel/typeops.ml                     | 4 +---
 pretyping/coercion.ml                 | 4 ++--
 pretyping/typing.ml                   | 3 +--
 proofs/logic.ml                       | 2 +-
 test-suite/failure/proofirrelevance.v | 5 ++---
 test-suite/success/Case19.v           | 2 +-
 10 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7eae9b8310..a290b240d8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -113,7 +113,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let check_inductive_type env t1 t2 =
 
-    (* Due to sort-polymorphism in inductive types, the conclusions of
+    (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
        of the types of the constructors.
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 173e19ce1b..9bb76ba721 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -278,13 +278,11 @@ let rec execute env cstr =
 	let j =
 	  match f with
 	    | Ind ind ->
-		(* Sort-polymorphism of inductive types *)
 		judge_of_inductive_knowing_parameters env ind jl
 	    | Const cst ->
-		(* Sort-polymorphism of constant *)
 		judge_of_constant_knowing_parameters env cst jl
 	    | _ ->
-		(* No sort-polymorphism *)
+		(* No template polymorphism *)
 		execute env f
 	in
         let jl = Array.map2 (fun c ty -> c,ty) args jl in
diff --git a/engine/universes.mli b/engine/universes.mli
index 932de941a6..83ca1ea606 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -223,7 +223,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 
-(** {6 Support for old-style sort-polymorphism } *)
+(** {6 Support for template polymorphism } *)
 
 val solve_constraints_system : universe option array -> universe array -> universe array ->
   universe array
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c8ceb064d5..d0fdf9fdae 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -117,7 +117,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name env t1 t2 =
 
-    (* Due to sort-polymorphism in inductive types, the conclusions of
+    (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
        of the types of the constructors.
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7d9a2aac09..dbc0dcb73e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -367,15 +367,13 @@ let rec execute env cstr =
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
-	      (* Template sort-polymorphism of inductive types *)
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_inductive_knowing_parameters env ind args
 	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
-	      (* Template sort-polymorphism of constants *)
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_constant_knowing_parameters env cst args
 	  | _ ->
-	    (* Full or no sort-polymorphism *)
+	    (* No template polymorphism *)
             execute env f
 	in
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdfa..f4514d7c07 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -479,8 +479,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
           (* We eta-expand (hence possibly modifying the original term!) *)
 	  (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
 	  (* has type forall (x:u1), u2 (with v' recursively obtained) *)
-          (* Note: we retype the term because sort-polymorphism may have *)
-          (* weaken its type *)
+          (* Note: we retype the term because template polymorphism may have *)
+          (* weakened its type *)
 	  let name = match name with
 	    | Anonymous -> Name Namegen.default_dependent_ident
 	    | _ -> name in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c2a030bcd2..00535adb7d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -313,14 +313,13 @@ let rec execute env evdref cstr =
 	let j =
 	  match EConstr.kind !evdref f with
 	    | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
-		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env !evdref (ind, u) jl)
 	    | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
-		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env !evdref (cst, u) jl)
 	    | _ ->
+                (* No template polymorphism *)
 		execute env evdref f
 	in
 	e_judge_of_apply env evdref j jl
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6024785db..d8c1f1f3b5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -379,7 +379,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
 	    let ty = 
-	      (* Template sort-polymorphism of definition and inductive types *)
+	      (* Template polymorphism of definitions and inductive types *)
 	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
 	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index b62f9b6867..bb9579d487 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,6 +1,5 @@
-(* This was working in version 8.1beta (bug in the Sort-polymorphism
-   of inductive types), but this is inconsistent with classical logic
-   in Prop *)
+(* This was working in version 8.1beta (bug in template polymorphism),
+   but this is inconsistent with classical logic in Prop *)
 
 Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
 with bool : Type := true : bool | false : bool.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index c29e529783..e59828defe 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -1,5 +1,5 @@
 (* This used to fail in Coq version 8.1 beta due to a non variable
-   universe (issued by the inductive sort-polymorphism) being sent by
+   universe (issued by template polymorphism) being sent by
    pretyping to the kernel (bug #1182) *)
 
 Variable T : Type.
-- 
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(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f36969e821..0441f952df 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(+)

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