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.
---
 kernel/typeops.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/typeops.ml')

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
 
-- 
cgit v1.2.3