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/entries.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/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 724ed9ec7..40873bea7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -75,7 +75,7 @@ type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.Named.t option; + const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -85,7 +85,7 @@ type 'a definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Context.Named.t option; + secdef_secctx : Constr.named_context option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -93,7 +93,7 @@ type section_def_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.Named.t option * types in_constant_universes_entry * inline + Constr.named_context option * types in_constant_universes_entry * inline type 'a constant_entry = | DefinitionEntry of 'a definition_entry |