diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-02 15:11:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-17 11:44:00 +0200 |
| commit | 4513b7735779fb440223e6f22079994528249047 (patch) | |
| tree | 101660d2dd2f1788d49c4b45ee4d62d7d142ebc2 /kernel/entries.ml | |
| parent | 74d700e9f7fcb14e7136e87b5efab25d5adb194b (diff) | |
Remove special declaration of primitive projections in the kernel.
This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7e..3c555f8c7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.Named.t option * types in_constant_universes_entry * inline -type projection_entry = { - proj_entry_ind : MutInd.t; - proj_entry_arg : int } - type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry - | ProjectionEntry of projection_entry (** {6 Modules } *) |