aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--API/API.mli5
-rw-r--r--checker/cic.mli4
-rw-r--r--checker/declarations.ml8
-rw-r--r--checker/environ.ml8
-rw-r--r--checker/environ.mli2
-rw-r--r--checker/mod_checking.ml14
-rw-r--r--checker/subtyping.ml4
-rw-r--r--checker/typeops.ml25
-rw-r--r--checker/typeops.mli3
-rw-r--r--checker/values.ml7
-rw-r--r--engine/termops.ml3
-rw-r--r--engine/universes.ml2
-rw-r--r--interp/impargs.ml2
-rw-r--r--kernel/cooking.ml23
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml16
-rw-r--r--kernel/environ.ml21
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml34
-rw-r--r--kernel/typeops.ml61
-rw-r--r--kernel/typeops.mli16
-rw-r--r--library/global.ml5
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--pretyping/evarsolve.ml6
-rw-r--r--pretyping/retyping.ml7
-rw-r--r--pretyping/typing.ml8
-rw-r--r--printing/prettyp.ml17
-rw-r--r--printing/printmod.ml2
-rw-r--r--vernac/assumptions.ml5
-rw-r--r--vernac/vernacentries.ml2
35 files changed, 65 insertions, 281 deletions
diff --git a/API/API.mli b/API/API.mli
index a042ad802..19726b52f 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