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 /engine | |
| 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 'engine')
| -rw-r--r-- | engine/termops.ml | 3 | ||||
| -rw-r--r-- | engine/universes.ml | 2 |
2 files changed, 1 insertions, 4 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 1aba2bbdd1..cf7c0cc20c 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 08461a2186..719af43edf 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 |