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/constr.mli | |
| 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/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index bf7b5e87b..70acf1932 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -372,6 +372,15 @@ val eq_constr_nounivs : constr -> constr -> bool (** Total ordering compatible with [equal] *) val compare : constr -> constr -> int +(** {6 Extension of Context with declarations on constr} *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list + (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] |