diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 58fb5d66b..95078800e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -80,7 +80,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) type constant_body = { - const_hyps : Context.Named.t; (** New: younger hyp at top *) + const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; @@ -138,7 +138,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -196,13 +196,13 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) + mind_hyps : Constr.named_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) |