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/declarations.ml | |
| parent | f0ae8e82ea53ce72ddac1fb8f7f40fd1beacf787 (diff) | |
| parent | e43710b391c278ac7fcb808ec28d720b4317660c (diff) | |
Merge PR #7714: Remove primitive-projection related data from the kernel
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd70c0502..7bd7d6c9ca 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -54,8 +54,6 @@ type projection_body = { proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) - proj_eta : constr * types; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility with VMs only, the match version *) } (* Global declarations (i.e. constants) can be either: *) @@ -87,7 +85,6 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for |