| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
One case missing due the TACTIC EXTEND macro.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
|
| |\ \ \
| |/ /
|/| | |
|
| | |\ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
|
| | | |\ \
| |_|/ /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| | |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | | |
RawLocal -> CLocal
|
| |/ / /
| | |
| | |
| | | |
This is a bit long, but it is to keep a symmetry with constr_expr.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
|
| |/ /
| |
| |
| |
| |
| | |
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Previously, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.
This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
No functional change, one extra copy introduced but it seems hard to
avoid.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
|
| | | | |
|
| | |
| |
| |
| | |
This is needed to fix `Declare ML Module "ltac_plugin".
|
| | |
| |
| |
| | |
Tactic Notation
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
|
| |
|
|
|
| |
This reverts commit e8137ae63b3b19436755f372b595e7343e942894,
was meant for 8.6 branch only.
|
| | |
|
| |
|
|
|
|
|
| |
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
Emilio Jesus Gallego Arias
Gaetan Gilbert
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Tej Chajed