diff options
| author | Pierre-Marie Pédrot | 2017-07-17 12:57:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 15:17:12 +0200 |
| commit | d9530632321c0b470ece6337cda2cf54d02d61eb (patch) | |
| tree | dd8ef37eddb9a3244c85e7cf042c5168edc95e12 /API/API.mli | |
| parent | 906b48ff401f22be6059a6cdde8723b858102690 (diff) | |
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.
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/API/API.mli b/API/API.mli index 4d9904b5f5..f2324bb449 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 |