From d9530632321c0b470ece6337cda2cf54d02d61eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Jul 2017 12:57:43 +0200 Subject: Removing template polymorphism for definitions. The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. --- kernel/typeops.mli | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'kernel/typeops.mli') 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 -- cgit v1.2.3