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.

9 files changed, 15 insertions, 60 deletions

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;