diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 02:37:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-27 22:01:36 +0200 |
| commit | 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 (patch) | |
| tree | 77f792ccddcc48229c08f321666c85debc4b008f /kernel/declarations.ml | |
| parent | c33988dafcad14f9f0c10a287d2cfb2790e253c4 (diff) | |
Swapping Context and Constr: defining declarations on constr in Constr.
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
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 *) |