Update various comments to use "template polymorphism"

Also remove obvious comments.

10 files changed, 12 insertions, 18 deletions

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7eae9b831..a290b240d 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 173e19ce1..9bb76ba72 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 932de941a..83ca1ea60 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 c8ceb064d..d0fdf9fda 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 7d9a2aac0..dbc0dcb73 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 542db7fdf..f4514d7c0 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 c2a030bcd..00535adb7 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 e6024785d..d8c1f1f3b 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 b62f9b686..bb9579d48 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 c29e52978..e59828def 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.