diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a7..7bd70c0502 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -52,7 +52,7 @@ type inline = int option type projection_body = { proj_ind : MutInd.t; proj_npars : int; - proj_arg : 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 *) @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for |