| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
comments.
[ci skip]
|
| |
| |
| |
| | |
[ci skip]
|
| |
| |
| |
| |
| |
| | |
Clarification prompted by Jim Fehrle.
[ci skip]
|
|\ \
| |/
|/|
| | |
in CArray
|
|\ \
| | |
| | |
| | | |
spawn timeout.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
instances
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
|\ \ \ \ \ \ \
| |_|_|_|_|/ /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This follows the model of smartmap and smartmap2.
|
| |_|_|_|_|_|/
|/| | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | | |
As per PR comment suggestion
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
|\ \ \ \ \ \ \
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This should hopefully alleviate memory problems on gitlab, by first
building the `lite` targets, and then building the remaining
not-that-big targets.
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / /
|/| | | | | | | |
| | | | | | | | | |
lib.cma).
|
| |_|_|_|_|_|_|/
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This closes #7580
c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and
https://github.com/coq/coq/pull/7559#issuecomment-390872924. This
should be reverted if and when we move to autogenerated docs for
warnings and errors, as suggested in #7373.
|
| | | | | | | | |
|
|\ \ \ \ \ \ \ \
| |/ / / / / / /
|/| | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
multiple lines
|
| |_|_|_|_|_|_|/ / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
It seems that it is standard practice in the OCaml world to set the
`-cclib` flags at library creation time, at least in native libraries.
Indeed, this seems to make linking easier as seen for example in #7563.
|
|\ \ \ \ \ \ \ \ \ \ |
|
| |/ / / / / / / / /
|/| | | | | | | | | |
|
| |_|_|_|/ / / / /
|/| | | | | | | | |
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
|/ / / / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
It is needed by Elpi and pidetop, and it is anyways needed for most
OCaml packages, including some Coq tools in the future.
The future base Docker image will include it by default.
|
|\ \ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Failed in v8.7.2 but were fixed by v8.8.0.
|
|\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
packaging scripts.
|
|\ \ \ \ \ \ \ \ \ \
| |_|/ / / / / / / /
|/| | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ |
|