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 /library/global.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 'library/global.ml')
| -rw-r--r-- | library/global.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |