| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \ |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
type is unknown
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
It made the test always fail so ci-common was always sourced. It's not
quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Actually, ocaml is apparently doing well. If there is a printer for 'a
Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined
existing ones, so, it is apparently not a problem to have overlapping
printer.
|
| |_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The two lines that this commit remove are spurious as a `git clean -dfx || true`
is already performed in `test-suite/coq-makefile/template/init.sh`.
While this resolves the accidental dependency on git, I am still unhappy with
this call of `git clean -dfx`.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
tac2 ]"
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
The message is the "Conversion test raised an anomaly" one.
|
| |_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | |
|
| |_|_|_|/ / / / / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | |_|/ /
| | | | | | | |/| | |
| | | | | | | | | | |
| | | | | | | | | | | |
We do up to `Term` which is the main bulk of the changes.
|
| |_|_|_|_|_|/ / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This will allow to merge back `Names` with `API.Names`
|
|\ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|/ / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
not "first [ progress tac1 | progress tac2 ]".
And add a missing backslash.
|
| |_|_|_|_|_|_|/ /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This is a temporary commit which should be reverted once the issue is fixed.
|
| |_|_|/ / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
alphabet).
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
rules
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | |
|
| |_|_|/ / / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
It is not clear that this is really needed, but in case it happens,
one will at least have a partial result available rather than an
unexploitable global failure of the parser.
|
| |_|_|/ / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Indeed, the debugger debugs coqtop but it is itself just an ocaml
runtime extended with the coq printers. It does not know the
environment, so, looking in the Global.env() for the printers can only
fail.
|
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | | |
|
| |_|_|/ / / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This is a first step towards some of the solutions proposed in #6008.
|
| |_|/ / / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | | |
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
|
| |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | | |
Adding a file fixing #5996 and which uses this feature.
|
|\ \ \ \ \ \ \ |
|