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.

35 files changed, 65 insertions, 281 deletions

diff --git a/API/API.mli b/API/API.mli
index 4d9904b5f..f2324bb44 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1185,8 +1185,6 @@ sig
     | RegularArity of 'a
     | TemplateArity of 'b
 
-  type constant_type = (Constr.types, Context.Rel.t * template_arity) declaration_arity
-
   type constant_universes =
     | Monomorphic_const of Univ.universe_context
     | Polymorphic_const of Univ.abstract_universe_context
@@ -1208,7 +1206,7 @@ sig
   type constant_body = {
         const_hyps : Context.Named.t;
         const_body : constant_def;
-        const_type : constant_type;
+        const_type : Term.types;
         const_body_code : Cemitcodes.to_patch_substituted option;
         const_universes : constant_universes;
         const_proj : projection_body option;
@@ -1586,7 +1584,6 @@ end
 module Typeops :
 sig
   val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment
-  val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types
   val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types
 end
 
diff --git a/checker/cic.mli b/checker/cic.mli
index 14fa7c774..59dd5bc4d 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -182,8 +182,6 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (constr, rel_context * template_arity) declaration_arity
-
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
 
@@ -226,7 +224,7 @@ type typing_flags = {
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
-    const_type : constant_type;
+    const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
     const_proj : projection_body option;
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2eefe4781..093d999a3 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -515,12 +515,6 @@ let subst_rel_declaration sub =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-let subst_template_cst_arity sub (ctx,s as arity) =
-  let ctx' = subst_rel_context sub ctx in
-    if ctx==ctx' then arity else (ctx',s)
-
-let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
-
 let constant_is_polymorphic cb =
   match cb.const_universes with
   | Monomorphic_const _ -> false
@@ -531,7 +525,7 @@ let constant_is_polymorphic cb =
 let subst_const_body sub cb =
  { cb with
     const_body = subst_constant_def sub cb.const_body;
-    const_type = subst_arity sub cb.const_type }
+    const_type = subst_mps sub cb.const_type }
 
 
 let subst_regular_ind_arity sub s =
diff --git a/checker/environ.ml b/checker/environ.ml
index d3f393c65..a0818012c 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -124,12 +124,6 @@ let constraints_of cb u =
   | Monomorphic_const _ -> Univ.Constraint.empty
   | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
-let map_regular_arity f = function
-  | RegularArity a as ar -> 
-    let a' = f a in 
-      if a' == a then ar else RegularArity a'
-  | TemplateArity _ -> assert false
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
@@ -137,7 +131,7 @@ let constant_type env (kn,u) =
   | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
   | Polymorphic_const ctx -> 
     let csts = constraints_of cb u in
-    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+    (subst_instance_constr u cb.const_type, csts)
 
 exception NotEvaluableConst of const_evaluation_result
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 754c295d2..8e8d0fd49 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -46,7 +46,7 @@ val check_constraints : Univ.constraints -> env -> bool
 (* Constants *)
 val lookup_constant : constant -> env -> Cic.constant_body
 val add_constant : constant -> Cic.constant_body -> env -> env
-val constant_type : env -> constant puniverses -> constant_type Univ.constrained
+val constant_type : env -> constant puniverses -> constr Univ.constrained
 type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant puniverses -> constr
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 4948f6008..b6816dd48 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -35,15 +35,11 @@ let check_constant_declaration env kn cb =
       push_context ~strict:false ctx env
   in
   let envty, ty = 
-    match cb.const_type with
-      RegularArity ty ->
-        let ty', cu = refresh_arity ty in
-        let envty = push_context_set cu env' in
-        let _ = infer_type envty ty' in envty, ty
-    | TemplateArity(ctxt,par) ->
-        let _ = check_ctxt env' ctxt in
-        check_polymorphic_arity env' ctxt par;
-	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
+    let ty = cb.const_type in
+    let ty', cu = refresh_arity ty in
+    let envty = push_context_set cu env' in
+    let _ = infer_type envty ty' in
+    envty, ty
   in
   let () = 
     match body_of_constant cb with
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 3097c3a0b..68a467bea 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -294,8 +294,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 	let cb1 = subst_const_body subst1 cb1 in
 	let cb2 = subst_const_body subst2 cb2 in
 	(*Start by checking types*)
-	let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-	let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+	let typ1 = cb1.const_type in
+	let typ2 = cb2.const_type in
 	check_type env typ1 typ2;
 	(* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
diff --git a/checker/typeops.ml b/checker/typeops.ml
index f2cbfec7d..9f39d588a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -69,35 +69,16 @@ let judge_of_relative env n =
 
 (* Type of constants *)
 
-
-let type_of_constant_type_knowing_parameters env t paramtyps =
-  match t with
-  | RegularArity t -> t
-  | TemplateArity (sign,ar) ->
-      let ctx = List.rev sign in
-      let ctx,s = instantiate_universes env ctx ar paramtyps in
-      mkArity (List.rev ctx,s)
-
-let type_of_constant_knowing_parameters env cst paramtyps =
-  let ty, cu = constant_type env cst in
-    type_of_constant_type_knowing_parameters env ty paramtyps, cu
-
-let type_of_constant_type env t =
-  type_of_constant_type_knowing_parameters env t [||]
-
-let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
+let judge_of_constant env (kn,u as cst) =
   let _cb =
     try lookup_constant kn env
     with Not_found ->
       failwith ("Cannot find constant: "^Constant.to_string kn)
   in
-  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+  let ty, cu = constant_type env cst in
   let () = check_constraints cu env in
     ty
 
-let judge_of_constant env cst =
-  judge_of_constant_knowing_parameters env cst [||]
-
 (* Type of an application. *)
 
 let judge_of_apply env (f,funj) argjv =
@@ -276,8 +257,6 @@ let rec execute env cstr =
 	  match f with
 	    | Ind ind ->
 		judge_of_inductive_knowing_parameters env ind jl
-	    | Const cst ->
-		judge_of_constant_knowing_parameters env cst jl
 	    | _ ->
 		(* No template polymorphism *)
 		execute env f
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 2be461b05..d9f2915a3 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -18,6 +18,3 @@ val infer_type : env -> constr      -> sorts
 val check_ctxt : env -> rel_context -> env
 val check_polymorphic_arity :
   env -> rel_context -> template_arity -> unit
-
-val type_of_constant_type : env -> constant_type -> constr
-
diff --git a/checker/values.ml b/checker/values.ml
index e13430e98..c95c3f1b2 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 67309b04a86b247431fd3e580ecbb50d  checker/cic.mli
+MD5 c802f941f368bedd96e931cda0559d67  checker/cic.mli
 
 *)
 
@@ -201,9 +201,6 @@ let v_engagement = v_impredicative_set
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
-let v_cst_type =
-  v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|]
-
 let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
@@ -222,7 +219,7 @@ let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_contex
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
-    v_cst_type;
+    v_constr;
     Any;
     v_const_univs;
     Opt v_projbody;
diff --git a/engine/termops.ml b/engine/termops.ml
index 1aba2bbdd..cf7c0cc20 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1145,9 +1145,6 @@ let is_template_polymorphic env sigma f =
   | Ind (ind, u) ->
     if not (EConstr.EInstance.is_empty u) then false
     else Environ.template_polymorphic_ind ind env
-  | Const (cst, u) ->
-    if not (EConstr.EInstance.is_empty u) then false
-    else Environ.template_polymorphic_constant cst env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
diff --git a/engine/universes.ml b/engine/universes.ml
index 08461a218..719af43ed 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -419,7 +419,7 @@ let type_of_reference env r =
   | VarRef id -> Environ.named_type id env, ContextSet.empty
   | ConstRef c ->
      let cb = Environ.lookup_constant c env in
-     let ty = Typeops.type_of_constant_type env cb.const_type in
+     let ty = cb.const_type in
      begin
        match cb.const_universes with
        | Monomorphic_const _ -> ty, ContextSet.empty
diff --git a/interp/impargs.ml b/interp/impargs.ml
index b7125fc85..d8241c044 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -414,7 +414,7 @@ let compute_semi_auto_implicits env f manual t =
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
   let cb = Environ.lookup_constant cst env in
-  let ty = Typeops.type_of_constant_type env cb.const_type in
+  let ty = cb.const_type in
   let impls = compute_semi_auto_implicits env flags manual ty in
     impls
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 63614e20f..80d41847c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -18,7 +18,6 @@ open Util
 open Names
 open Term
 open Declarations
-open Environ
 open Univ
 
 module NamedDecl = Context.Named.Declaration
@@ -153,7 +152,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
@@ -167,11 +166,6 @@ let on_body ml hy f = function
     OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
-let constr_of_def otab = function
-  | Undef _ -> assert false
-  | Def cs -> Mod_subst.force_constr cs
-  | OpaqueDef lc -> Opaqueproof.force_proof otab lc
-
 let expmod_constr_subst cache modlist subst c =
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
@@ -220,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } =
       List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
       hyps ~init:cb.const_hyps in
-  let typ = match cb.const_type with
-    | RegularArity t ->
-  	let typ =
-          abstract_constant_type (expmod t) hyps in
-  	RegularArity typ
-    | TemplateArity (ctx,s) ->
-  	let t = mkArity (ctx,Type s.template_level) in
-  	let typ = abstract_constant_type (expmod t) hyps in
-  	let j = make_judge (constr_of_def (opaque_tables env) body) typ in
-  	Typeops.make_polymorphic_if_constant_for_ind env j
-  in
+  let typ = abstract_constant_type (expmod cb.const_type) hyps in
   let projection pb =
     let c' = abstract_constant_body (expmod pb.proj_body) hyps in
     let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
@@ -244,9 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
 	  | _ -> assert false 
       with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
     in 
-    let typ = (* By invariant, a regular arity *)
-      match typ with RegularArity t -> t | TemplateArity _ -> assert false 
-    in
     let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_eta = etab, etat;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f386fd936..6d1b776c0 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f35438dfc..9697b0b8b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
-
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
 
@@ -83,7 +81,7 @@ type typing_flags = {
 type constant_body = {
     const_hyps : Context.Named.t; (** New: younger hyp at top *)
     const_body : constant_def;
-    const_type : constant_type;
+    const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
     const_proj : projection_body option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index efce21982..85dd1e66d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -69,10 +69,6 @@ let subst_rel_declaration sub =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-let subst_template_cst_arity sub (ctx,s as arity) =
-  let ctx' = subst_rel_context sub ctx in
-    if ctx==ctx' then arity else (ctx',s)
-      
 let subst_const_type sub arity =
   if is_empty_subst sub then arity
   else subst_mps sub arity
@@ -94,7 +90,7 @@ let subst_const_body sub cb =
   if is_empty_subst sub then cb
   else
     let body' = subst_const_def sub cb.const_body in
-    let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in
+    let type' = subst_const_type sub cb.const_type in
     let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
       && proj' == cb.const_proj then cb
@@ -120,14 +116,6 @@ let hcons_rel_decl =
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
-let hcons_regular_const_arity t = Term.hcons_constr t
-
-let hcons_template_const_arity (ctx, ar) = 
-  (hcons_rel_context ctx, hcons_template_arity ar)
-
-let hcons_const_type = 
-  map_decl_arity hcons_regular_const_arity hcons_template_const_arity
-
 let hcons_const_def = function
   | Undef inl -> Undef inl
   | Def l_constr ->
@@ -145,7 +133,7 @@ let hcons_const_universes cbu =
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
-    const_type = hcons_const_type cb.const_type;
+    const_type = Term.hcons_constr cb.const_type;
     const_universes = hcons_const_universes cb.const_universes }
 
 (** {6 Inductive types } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b01b65200..d2c737ab0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,12 +232,6 @@ let constraints_of cb u =
   | Monomorphic_const _ -> Univ.Constraint.empty
   | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
-let map_regular_arity f = function
-  | RegularArity a as ar -> 
-    let a' = f a in 
-      if a' == a then ar else RegularArity a'
-  | TemplateArity _ -> assert false
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
@@ -245,7 +239,7 @@ let constant_type env (kn,u) =
   | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
   | Polymorphic_const ctx -> 
     let csts = constraints_of cb u in
-    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+    (subst_instance_constr u cb.const_type, csts)
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
@@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) =
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
+	b', subst_instance_constr u cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if Declareops.constant_is_polymorphic cb then
-      map_regular_arity (subst_instance_constr u) cb.const_type
+      subst_instance_constr u cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env =
 let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
-let template_polymorphic_constant cst env =
-  match (lookup_constant cst env).const_type with 
-  | TemplateArity _ -> true
-  | RegularArity _ -> false
-
-let template_polymorphic_pconstant (cst,u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else template_polymorphic_constant cst env
-
 let lookup_projection cst env =
   match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cd7a9d279..377c61de2 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} *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index c7f3e5c51..0888ccc10 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -83,7 +83,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let c',cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      j.uj_val, cst'
@@ -103,7 +103,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bd82dd465..b311165f1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -313,8 +313,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
           error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let typ1 = cb1.const_type in
+      let typ2 = cb2.const_type in
       let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43c099712..3f42c348f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,7 +21,6 @@ open Environ
 open Entries
 open Typeops
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
@@ -128,7 +127,7 @@ let inline_side_effects env body ctx side_eff =
       match cb.const_universes with
       | Monomorphic_const cnstctx ->
         (** Abstract over the term at the top of the proof *)
-        let ty = Typeops.type_of_constant_type env cb.const_type in
+        let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
         let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
@@ -249,7 +248,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
       {
         Cooking.cook_body = Undef nl;
-        cook_type = RegularArity t;
+        cook_type = t;
         cook_proj = None;
         cook_universes = univs;
         cook_inline = false;
@@ -290,7 +289,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       {
         Cooking.cook_body = def;
-        cook_type = RegularArity typ;
+        cook_type = typ;
         cook_proj = None;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
@@ -320,13 +319,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not poly then (* Old-style polymorphism *)
-             make_polymorphic_if_constant_for_ind env j
-           else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+          Vars.subst_univs_level_constr usubst j.uj_type
         | Some t ->
            let tj = infer_type env t in
            let _ = judge_of_cast env j DEFAULTcast tj in
-           RegularArity (Vars.subst_univs_level_constr usubst t)
+           Vars.subst_univs_level_constr usubst t
       in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
@@ -363,21 +360,13 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
     let term, typ = pb.proj_eta in
     {
       Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
-      cook_type = RegularArity typ;
+      cook_type = typ;
       cook_proj = Some pb;
       cook_universes = univs;
       cook_inline = false;
       cook_context = None;
     }
 
-let global_vars_set_constant_type env = function
-  | RegularArity t -> global_vars_set env t
-  | TemplateArity (ctx,_) ->
-      Context.Rel.fold_outside
-        (RelDecl.fold_constr
-	  (fun t c -> Id.Set.union (global_vars_set env t) c))
-      ctx ~init:Id.Set.empty
-
 let record_aux env s_ty s_bo suggested_expr =
   let in_ty = keep_hyps env s_ty in
   let v =
@@ -426,7 +415,7 @@ let build_constant_declaration kn env result =
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
-        let ids_typ = global_vars_set_constant_type env typ in
+        let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
@@ -454,14 +443,14 @@ let build_constant_declaration kn env result =
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
@@ -524,8 +513,7 @@ let constant_entry_of_side_effect cb u =
     const_entry_body = Future.from_val (pt, ());
     const_entry_secctx = None;
     const_entry_feedback = None;
-    const_entry_type =
-      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -625,7 +613,7 @@ let translate_recipe env kn r =
 let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
-  let typ = type_of_constant_type env decl.cook_type in
+  let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
     match decl.cook_body with
     | Undef _ -> ()
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b814deb6e..044877e82 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign =
 (* Type of constants *)
 
 
-let type_of_constant_type_knowing_parameters env t paramtyps =
-  match t with
-  | RegularArity t -> t
-  | TemplateArity (sign,ar) ->
-      let ctx = List.rev sign in
-      let ctx,s = instantiate_universes env ctx ar paramtyps in
-      mkArity (List.rev ctx,s)
-
-let type_of_constant_knowing_parameters env (kn,u as cst) args =
+let type_of_constant env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   let ty, cu = constant_type env cst in
-  let ty = type_of_constant_type_knowing_parameters env ty args in
   let () = check_constraints cu env in
     ty
 
-let type_of_constant_knowing_parameters_in env (kn,u as cst) args =
+let type_of_constant_in env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
-  let ty = constant_type_in env cst in
-  type_of_constant_type_knowing_parameters env ty args
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
-  type_of_constant_knowing_parameters_in env cst [||]
-
-let type_of_constant_type env t =
-  type_of_constant_type_knowing_parameters env t [||]
+  constant_type_in env cst
 
 (* Type of a lambda-abstraction. *)
 
@@ -369,9 +350,6 @@ let rec execute env cstr =
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    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 ->
-	    let args = Array.map (fun t -> lazy t) argst in
-              type_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* No template polymorphism *)
             execute env f
@@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
 let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
 
 let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst)
-let judge_of_constant_knowing_parameters env cst args =
-  make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args)
 
 let judge_of_projection env p cj =
   make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type)
@@ -559,34 +535,3 @@ let type_of_projection_constant env (p,u) =
       Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-(* Instantiation of terms on real arguments. *)
-
-(* Make a type polymorphic if an arity *)
-
-let extract_level env p =
-  let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
-
-let extract_context_levels env l =
-  let fold l = function
-    | RelDecl.LocalAssum (_,p) -> extract_level env p :: l
-    | RelDecl.LocalDef _ -> l
-  in
-  List.fold_left fold [] l
-
-let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
-  let params, ccl = dest_prod_assum env t in
-  match kind_of_term ccl with
-  | Sort (Type u) ->
-     let ind, l = decompose_app (whd_all env c) in
-     if isInd ind && List.is_empty l then
-       let mis = lookup_mind_specif env (fst (destInd ind)) in
-       let nparams = Inductive.inductive_params mis in
-       let paramsl = CList.lastn nparams params in
-       let param_ccls = extract_context_levels env paramsl in
-       let s = { template_param_levels = param_ccls; template_level = u} in
-       TemplateArity (params,s)
-     else RegularArity t
-  | _ ->
-      RegularArity t
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 24521070e..a8f7fba9a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -11,7 +11,6 @@ open Univ
 open Term
 open Environ
 open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
 
@@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 
 val judge_of_constant : env -> pconstant -> unsafe_judgment
 
-val judge_of_constant_knowing_parameters :
-  env -> pconstant -> types Lazy.t array -> unsafe_judgment
-
 (** {6 type of an applied projection } *)
 
 val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
@@ -98,21 +94,9 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_constant_type : env -> constant_type -> types
-
 val type_of_projection_constant : env -> Names.projection puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types
 
-val type_of_constant_type_knowing_parameters :
-  env -> constant_type -> types Lazy.t array -> types
-
-val type_of_constant_knowing_parameters_in :
-  env -> pconstant -> types Lazy.t array -> types
-
-(** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
-  constant_type
-
 (** Check that hyps are included in env and fails with error otherwise *)
 val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit
diff --git a/library/global.ml b/library/global.ml
index 00a3a4986..963c97741 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -199,8 +199,7 @@ let type_of_global_in_context env r =
   | ConstRef c -> 
     let cb = Environ.lookup_constant c env in 
     let univs = Declareops.constant_polymorphic_context cb in
-    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
-    Typeops.type_of_constant_type env cb.Declarations.const_type, univs
+    cb.Declarations.const_type, univs
   | IndRef ind ->
     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
     let univs = Declareops.inductive_polymorphic_context mib in
@@ -255,7 +254,7 @@ let is_template_polymorphic r =
   let env = env() in 
   match r with
   | VarRef id -> false
-  | ConstRef c -> Environ.template_polymorphic_constant c env
+  | ConstRef c -> false
   | IndRef ind -> Environ.template_polymorphic_ind ind env
   | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39826d744..89c2a0ae3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -132,7 +132,7 @@ let rec add_labels mp = function
 exception Impossible
 
 let check_arity env cb =
-  let t = Typeops.type_of_constant_type env cb.const_type in
+  let t = cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3661faada..661842790 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -518,7 +518,7 @@ and mlt_env env r = match r with
         match lookup_typedef kn cb with
         | Some _ as o -> o
         | None ->
-           let typ = Typeops.type_of_constant_type env cb.const_type
+           let typ = cb.const_type
            (* FIXME not sure if we should instantiate univs here *) in
 	   match flag_of_type env typ with
 	   | Info,TypeScheme ->
@@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ =
   | Some schema -> schema
   | None ->
      let typ = match opt_typ with
-       | None -> Typeops.type_of_constant_type env cb.const_type
+       | None -> cb.const_type
        | Some typ -> typ
      in
      let mlt = extract_type env [] 1 typ [] in
@@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 
 let extract_constant env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
   in
@@ -1025,7 +1025,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   try
     match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 863c9dc8d..89537ad3f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -857,7 +857,7 @@ let make_graph (f_ref:global_reference) =
 	   with_full_print (fun () ->
 		(Constrextern.extern_constr false env sigma body,
 		 Constrextern.extern_type false env sigma
-                   ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
+                   ((*FIXME*) c_body.const_type)
 		)
 	     )
 	     ()
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
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 827c0e458..17249262e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -501,9 +501,6 @@ let print_body env evd = function
 let print_typed_body env evd (val_0,typ) =
   (print_body env evd val_0 ++ fnl () ++ str "     : " ++ pr_ltype_env env evd typ)
 
-let ungeneralized_type_of_constant_type t = 
-  Typeops.type_of_constant_type (Global.env ()) t
-
 let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
     let univs = Declareops.constant_polymorphic_context cb in
@@ -515,17 +512,13 @@ let print_instance sigma cb =
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
-  let typ = match cb.const_type with
-  | RegularArity t as x ->
-    begin match cb.const_universes with
-    | Monomorphic_const _ -> x
+  let typ =
+    match cb.const_universes with
+    | Monomorphic_const _ -> cb.const_type
     | Polymorphic_const univs ->
       let inst = Univ.AUContext.instance univs in
-      RegularArity (Vars.subst_instance_constr inst t)
-    end
-  | TemplateArity _ as x -> x
+      Vars.subst_instance_constr inst cb.const_type
   in
-  let typ = ungeneralized_type_of_constant_type typ in
   let univs =
     let otab = Global.opaque_tables () in
     match cb.const_body with
@@ -698,7 +691,7 @@ let print_full_pure_context () =
       | "CONSTANT" ->
 	  let con = Global.constant_of_delta_kn kn in
 	  let cb = Global.lookup_constant con in
-	  let typ = ungeneralized_type_of_constant_type cb.const_type in
+	  let typ = cb.const_type in
 	  hov 0 (
 	    match cb.const_body with
 	      | Undef _ ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5c7dcdc10..219eafda4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -323,7 +323,7 @@ let print_body is_impl env mp (l,body) =
 	    str " :" ++ spc () ++
 	    hov 0 (Printer.pr_ltype_env env sigma
 		(Vars.subst_instance_constr u
-   		  (Typeops.type_of_constant_type env cb.const_type))) ++
+   		  cb.const_type)) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 86bbf46a3..6711b14da 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -311,10 +311,7 @@ let traverse current t =
 (** Hopefully bullet-proof function to recover the type of a constant. It just
     ignores all the universe stuff. There are many issues that can arise when
     considering terms out of any valid environment, so use with caution. *)
-let type_of_constant cb = match cb.Declarations.const_type with
-| Declarations.RegularArity ty -> ty
-| Declarations.TemplateArity (ctx, arity) ->
-  Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+let type_of_constant cb = cb.Declarations.const_type
 
 let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
   let (idts, knst) = st in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9650ea19d..6b04ff00a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -257,7 +257,7 @@ let print_namespace ns =
   in
   let print_constant k body =
     (* FIXME: universes *)
-    let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in
+    let t = body.Declarations.const_type in
     print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
   in
   let matches mp = match match_modulepath ns mp with