| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |_|_|_|/ /
|/| | | | | |
|
| |/ / / /
|/| | | | |
|
| |/ / /
|/| | |
| | | | |
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.
However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479
Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.
This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
| |\ \ \ |
|
|\ \ \ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This fixes a logical error introduced in
ce2b2058587224ade9261cd4127ef4f6e94d356b
Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Indeed we were not correctly backtracking in the case of
StackOverflow. It makes sense to remove the inner handler which is a
leftover of a previous attempt, and handle interpretation errors in
load as non-recoverable.
This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
|
| |_|_|/
|/| | |
| | | |
| | | | |
The only use in Equality is reimplemented in the new engine.
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | |\ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
We now test:
- 4.02.3 + 6.14 [and 32bits of those]
- 4.04.0 + 6.17
this looks like what the official support set should be for 8.7, given
that both Ubuntu and Debian will ship the first, then switch to the
latter.
We also pin xmlm to version 1.2.0 to workaround bug
https://github.com/ocaml/opam-repository/issues/8815
|
| | |/ / / / / / / / / / /
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
In 8.6 + emacs, errors were quoted sometimes with special
markers (e.g. `Print Module foo.` for a non-existing `foo`)
In 8.7 we uniformized error handling and now all errors are quoted,
however, this behavior confuses emacs as it seems that the quotes are
meant to be applied only to warnings.
We thus reflect the de-facto situation, removing quoting for errors
and updating the code so it is clear that the quoter is a warnings
quoter. We also update the warnings quoter to use a warning tag
instead of a non-printable char.
This fixes ProofGeneral for trunk users.
c.f. https://github.com/ProofGeneral/PG/issues/175
|