diff options
| author | Maxime Dénès | 2018-06-19 08:27:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-19 08:27:51 +0200 |
| commit | 981864d47efca1d42f43dc5b7c5439638a86f315 (patch) | |
| tree | a835613a0143b6cfc2ab8f94361afda62840954e /kernel/entries.ml | |
| parent | f0ae8e82ea53ce72ddac1fb8f7f40fd1beacf787 (diff) | |
| parent | e43710b391c278ac7fcb808ec28d720b4317660c (diff) | |
Merge PR #7714: Remove primitive-projection related data from the kernel
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 94da00c7eb..3c555f8c7b 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 } *) |