| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
It looks like the recent spurious failures are because it somehow
wants to build gramlib byte and opt at the same time and the old race
condition causes the error.
Having failed to debug the makefile, we work around by building byte first.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
This is the identity function since 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
repository
Reviewed-by: SkySkimmer
Ack-by: ejgallego
|
|
This improves reproducibility of the CI environment.
The chosen commit has GTK+3 at 2.24.9.
|
|
Reviewed-by: SkySkimmer
|
|
This removes spurious Ack-by lines
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
|
|
Reviewed-by: SkySkimmer
|
|
creation.
Reviewed-by: herbelin
|
|
|
|
|
|
We can statically enforce that opaque definitions are always impure by
means of typing, leading to quite a few simplifications.
|
|
This is the last call to the kernel that makes a difference between opaque
definitions depending on their polymorphic status.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
module.
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
command line (part 1)
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
|
|
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)
|
|
|
