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 /checker/declarations.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 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 2eefe4781..093d999a3 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -515,12 +515,6 @@ let subst_rel_declaration sub = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - -let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s - let constant_is_polymorphic cb = match cb.const_universes with | Monomorphic_const _ -> false @@ -531,7 +525,7 @@ let constant_is_polymorphic cb = let subst_const_body sub cb = { cb with const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type } + const_type = subst_mps sub cb.const_type } let subst_regular_ind_arity sub s = |