| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
with apt.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This one is a bit weird.
Unused since 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (kept semantics,
the m is the same one outside and inside the call)
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
(Universes and Evd)
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Unused since 2285dae8af54043090ce5f8a59aa4162679714c6
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The function is defined with a typo but called with the same env that
is mistakenly not shadowed.
An alternative to this commit would be to fix the typo.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Unused since d95306323 (remove template polymorphic definitions).
|
| | | | | | | |
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
compilers
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Unused since 8e07227c5853de78eaed4577eefe908fb84507c0.
|
| | | | | | | | |
|
| |_|_|/ / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Unused since fe1979bf47951352ce32a6709cb5138fd26f311d.
I'm not sure if it was actually used back then since I didn't look at
the function it was passed to.
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
./configure and make install not run yet
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This should help towards ensuring that the system only has the
packages we specify in the Dockerfile.
We were missing:
- `git`: used in the CI system itself!
- `rsync`: used in the test-suite
- `python3-setuptools`, `python3-wheel`: necessary to use pip3
properly to install the missing python package.
- `autoconf`, `automake`: a few CI contribs depend on them.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
It was forcing the macro to generate code that was useless.
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | |/ / / / |
|
| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
- move `README` to `README.md` to take advantage of markdown features
- remove `setup.txt`, port the editor specific information to the wiki.
Merge development information into `dev/doc/README.md`.
Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup.
- Add new links to files into `dev/README.md`.
- Remove stale `translate.txt`.
|
| | | | | | | | | | | |
|
| |_|_|_|_|/ / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|