| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.
Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.
The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
|
|
|
|
In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.
The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
|
|
This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.
Incidentally fixes #12649.
|
|
Add headers to a few files which were missing them.
|
|
We remove two flags that were seldom used in favor of named parameters.
|
|
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
|
|
|
|
|
|
|
|
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
|
|
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).
|
|
Highly spaghetti code, hopefully works.
|
|
This API is a bit strange, I expect it will change at some point.
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
|
|
|
|
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
|
|
|
|
|
|
|
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
|
|
|
|
This is a bit long, but it is to keep a symmetry with constr_expr.
|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
