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.
---
 pretyping/typing.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1bb0035751..1f35fa19aa 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,11 +35,6 @@ let meta_type evd mv =
   let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
-let constant_type_knowing_parameters env sigma (cst, u) jl =
-  let u = Unsafe.to_instance u in
-  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
-  EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp)
-
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
@@ -315,9 +310,6 @@ let rec execute env evdref cstr =
 	    | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
 		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 ->
-		make_judge f
-		  (constant_type_knowing_parameters env !evdref (cst, u) jl)
 	    | _ ->
                 (* No template polymorphism *)
 		execute env evdref f
-- 
cgit v1.2.3