| Commit message (Collapse) | Author | Age |
... | |
| | | |
|
|\ \ \
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
top of the linking chain.
|
|\ \ \ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
- timing needs time and python
- check for compiled files without source looks in the install
directory (except for make -f Makefile.ci which doesn't check), as
such the install directory has been renamed to _install_ci and isn't
searched.
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The OSX binaries were signed twice with a fake identity, leading to some
obscure errors on Travis in some cases.
We disable code signing for Travis artifacts. For released packages,
a proper signing will be applied manually.
|
| |_|_|/ /
|/| | | | |
|
|\ \ \ \ \ |
|
| | | | | | |
|
|\ \ \ \ \ \ |
|
| |_|_|_|_|/
|/| | | | | |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
|\ \ \ \ |
|
| | | | | |
|
| | |_|/
| |/| |
| | | |
| | | | |
linking chain.
|
| | | | |
|
|/ / /
| | |
| | | |
With a minimal diff (so I'm not putting quotes ` ` around all the code).
|
| |/
|/|
| |
| |
| | |
And remove old French part.
And move part about the plugin API to the right section.
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|