| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
We remove some unnecessary functions introduced before in the patch
series + unused functions.
|
|
|
|
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
|
Thanks to @gasche
|
|
|
|
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
|
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
|
Now it is a private field, locations are optional.
|
|
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.
|
|
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
|
