| Age | Commit message (Collapse) | Author |
|---|
|
Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
|
|
This is now the "coqidetop" binary which specifically know how to
collect extra arguments.
|
|
- Binding coqc execution to the generic support for Coq binaries
(i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
can avoid to call it. By the way, it is unclear what workerloop
should do with it. Also, it is unclear how much the -l option should
be considered an coqidetop or coq*worker option. In any case, it
should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
phase. Seems ok, despites the few involved side effects.
|
|
We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
|
|
|
|
Incidentally moving parsing of "-batch" to the coqtop binary.
|
|
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
|
|
|
|
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
|
|
|
|
|
|
|
|
for list prints in gramlib
Reviewed-by: ejgallego
|
|
Compcert needs a new menhir.
|
|
Order
Reviewed-by: Zimmi48
|
|
gramlib
This means we don't need to ignore the result of the fold. cf #10471
Using Format.pp_print_list instead of a custom iteri was suggested by
Jean-Christophe Léchenet (eponier)
|
|
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
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.
|
