From d9530632321c0b470ece6337cda2cf54d02d61eb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Jul 2017 12:57:43 +0200
Subject: Removing template polymorphism for definitions.

The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.

Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
---
 kernel/environ.mli | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index cd7a9d2791..377c61de2c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -139,10 +139,6 @@ val polymorphic_constant  : constant -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
 val type_in_type_constant : constant -> env -> bool
 
-(** Old-style polymorphism *)
-val template_polymorphic_constant  : constant -> env -> bool
-val template_polymorphic_pconstant : pconstant -> env -> bool
-
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -153,11 +149,11 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> constant_type constrained
+val constant_type : env -> constant puniverses -> types constrained
 
 val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
 val constant_value_and_type : env -> constant puniverses -> 
-  constr option * constant_type * Univ.constraints
+  constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> constant -> Univ.abstract_universe_context
@@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_universe_context
    already contains the constraints corresponding to the constant 
    application. *)
 val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> constant_type
+val constant_type_in : env -> constant puniverses -> types
 val constant_opt_value_in : env -> constant puniverses -> constr option
 
 (** {6 Primitive projections} *)
-- 
cgit v1.2.3