| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
One case missing due the TACTIC EXTEND macro.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| |
|
|
|
| |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| |
|
|
|
|
|
|
|
| |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
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
|
| |\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Note: I removed what seemed to be dead code in recdef.ml (local_assum
and local_def introduced with econstr branch), assuming that this is
what should be done.
|
| | |_|/ / / / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Hoping this is ok for everyone, otherwise we can discuss about it.
|
| | |_|/ / / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This warning is a special case as it happens outside the execution
context.
We could move the check inside, but instead we opt for the simpler
solution of properly setting the warning target.
|
| | |_|/ / / / /
|/| | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | |_|_|/ / /
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We again remove another user of Stateid.dummy. However, we need to
adapt the protocol so `Coq.query` takes the `route_id` and we can
redirect the output properly to the subwindow.
|
| | | | |_|/
| | |/| |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In particular, we set queries from the menu to the tip of the
document, and process feedback coming with a `dummy` id.
There are still more places to tweak, but this should be good for now.
We also display a few more query messages, in particular the feedbacks
produced by query that carry a dummy state id.
This hack of reporting with from the STM should be solved once we
update the protocol.
|
| | | |/ / |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
discharge literal comparisons.
|
| | | | |\ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \
| |_|_|_|_|_|/
|/| | | | | | |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
PR #441 and #530 had an interesting interaction creating two bugs:
- #441 stopped emitting feedback for the parser, however #530 changed
the mechanism to print parser errors to the feedback, thus when the
two patches were applied, parsing errors were not printed in
batch_mode.
- Additionally, #530 contains an error: prior to `Stm.init` we must
take care of exceptions `require ()`/etc... otherwise they won't get
printed.
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | | |
This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e,
`Notice`-level messages should not be wrapped in `<infomsg>` tags.
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | | |
The bug has been solved as a side-effect of the EConstr branch.
|
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Gaetan Gilbert
Matej Kosik
Pierre-Marie Pédrot
Théo Zimmermann