| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
The object was mostly for wrangling universes, but we already have the
universe object for that.
It's also used by some code which iterates over objects to find
variables.
Search used to do this but was changed in a previous commit.
Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
|
|
In preparation for the other declarations to use it.
|
|
In preparation for removing the VARIABLE object.
It seems this doesn't change the output tests.
|
|
The caller should push them first
|
|
Not sure what this was for.
|
|
This is the only use of restrict_path so we just remove it.
The name collision between Libnames.make_path (takes a dirpath) and
Lib.make_path (uses current module+section path) is a bit awkward...
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
module name.
Reviewed-by: SkySkimmer
|
|
|
|
Global.universes()
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: gares
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
We are not supposed to have any script depending specifically on python2.
|
|
|
|
We should have this in the check target, but meanwhile we have to do
manual housekeeping here.
|
|
We cleanup a few imports on Declare, and indeed we find a suspicious
exception `AlreadyDeclared` present in `CErrors` where it should not
be there.
We move it to `Declare`, waiting for more investigation.
|
|
is ambiguous with new one
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
new one
|
|
`declare_definition` didn't improve a lot the declare path and was
used only once on interesting code. Also, it had many optional
parameters. The declare path is critical enough as to care about a
tidy API.
|
|
We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.
|
|
We remove two flags that were seldom used in favor of named parameters.
|
|
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
|
|
The whole business of cst_kind is fishy tho, it seems to me that it
should be removed from the libobject path.
|
|
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.
|
|
See discussion in #10417
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
|
|
Reviewed-by: cpitclaudel
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
The old code was conditionally dumping and catching `Not_found`, as
noted by Gaëtan Gilbert on #10433:
> we could just remove the dump, the sibling functions
> (`full_extraction`, etc...) don't bother to dump for instance.
|
|
|
|
the kernel
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
State is still token except for proofs [due to the compat layer, would
be great if someone could port the STM], but this should be good for now.
|
|
main path
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.
Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
|
|
All section definitions are always defined as if they were transparent,
all the additional checks were actually never triggered.
|
|
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
