diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-17 12:57:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:17:12 +0200 |
| commit | d9530632321c0b470ece6337cda2cf54d02d61eb (patch) | |
| tree | dd8ef37eddb9a3244c85e7cf042c5168edc95e12 /pretyping/typing.ml | |
| 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 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 8 |
1 files changed, 0 insertions, 8 deletions
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 |