| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | | |
It is no longer accepted by Coq's ./configure.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
The Software Foundations archive has been replaced by three volumes.
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|\ \ |
|
| | | |
|
| | | |
|
|/ /
| |
| | |
With a minimal diff (so I'm not putting quotes ` ` around all the code).
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Not sure entirely what it was supposed to do, but stripping the newline
erased the following line
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Now the folded line starts with "Aggregating..." and not with
"---------"
|
| | | | |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The packages will be built only for main branches (not pull requests),
and are accessible via bintray: https://bintray.com/coq/coq
|
|/ / / / |
|
| | | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
This makes it so that when a ci target fails, we don't get red herring
error messages about .ok files not existing.
Since this requires bash, we make a helper script that invokes bash, so
as to not depend on bash in general.
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
db_printers just isn't used.
api.txt is superseded by the API OCaml interface.
|
| | |
| | |
| | |
| | | |
This gives syntax highlighting in Coq-aware editors.
|
| | | |
|
| | |
| | |
| | |
| | | |
Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
|
|/ /
| |
| |
| | |
They seem unused since 8f4b7f1 (2007).
|
|/
|
|
| |
This allows better debugging when it fails.
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |_|_|_|_|/
|/| | | | |
| | | | | |
| | | | | | |
Minor clean up, no sense in having these as they do nothing.
|
| |_|/ / /
|/| | | | |
|
| | | | | |
|
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| | | | |
| | | | |
| | | | |
| | | | | |
This puts the boilerplate all in one place
|
| | | | |
| | | | |
| | | | |
| | | | | |
HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
HoTT, which builds it's own makefile, and supports timing data, makes
use of its own timing script.
Everything else goes through the coq-bundled timing scripts.
|
| |_|_|/
|/| | | |
|
|\ \ \ \ |
|
| | | | | |
|