| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |\ |
|
| | | | |
|
| | |\ \ |
|
| | | | | |
|
| |\| | | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Also adding spaces around ":=" and ":" when printed as "(x : t := c)".
Example:
Check fun y => let x : True := I in fun z => z+y=0.
(* λ (y : nat) (x : True := I) (z : nat), z + y = 0
: nat → nat → Prop *)
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | | |
| | |
| | |
| | | |
RawLocal -> CLocal
|
| | | |
| | |
| | |
| | | |
This is a bit long, but it is to keep a symmetry with constr_expr.
|
| | |/ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| | |
| |
| |
| |
| | |
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | |
| |
| |
| |
| | |
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |\ |
|
| | | |\ |
|
| | | | | |
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | | |
became mandatory.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
with user-level notations by inserting spaces.
|
| | | | | |
|
| | | | | |
|
| |/| | |
| |/ / |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | | |
| | | |
| | | |
| | | | |
The option can be turned on by the user though.
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
Maxime Dénès
Guillaume Melquiond
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre Courtieu
Pierre-Marie Pédrot
Matthieu Sozeau