diff options
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 7bd70c050..7bd7d6c9c 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 |