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.

3 files changed, 1 insertions, 20 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f4829761..ef0fb8ea6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f =
       (match oib.mind_arity with
       | RegularArity _ -> assert false
       | TemplateArity templ -> templ.template_param_levels)
-  | Const (cst, u) ->
-    let cb = Global.lookup_constant cst in
-      (match cb.const_type with
-      | RegularArity _ -> assert false
-      | TemplateArity (_, templ) -> 
-        templ.template_param_levels)
   | _ -> assert false
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e0f9bfcb7..079524f34 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -192,11 +192,6 @@ let retype ?(polyprop=true) sigma =
 	EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
 	       ~polyprop env (mip, u) argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
-    | Const (cst, u) ->
-        let u = EInstance.kind sigma u in
-	EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps
-	 with Reduction.NotArity -> retype_error NotAnArity)
-    | Var id -> type_of_var env id
     | Construct (cstr, u) ->
       let u = EInstance.kind sigma u in
       EConstr.of_constr (type_of_constructor env (cstr, u))
@@ -220,7 +215,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
     | Const (cst, u) ->
         let t = constant_type_in env (cst, EInstance.kind sigma u) in
         (* TODO *)
-          sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||])
+          sigma, EConstr.of_constr t
     | Var id -> sigma, type_of_var env id
     | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
     | _ -> assert false
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1bb003575..1f35fa19a 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