| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
|
| |\ |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| |\ |
|
| | |\ |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
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.
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#337: Fix arguments
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
It now prints evars with candidates as well if there are any.
|
| |\| | | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
(It should apply also interactively.)
|
| | | |
| | |
| | |
| | |
| | | |
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
|
| |\| | |
|
| | | | |
|
| | |\ \
| | | |
| | | |
| | | |
| | | | |
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
| |\| | | |
|
Hugo Herbelin
Maxime Dénès
Guillaume Melquiond
Emilio Jesus Gallego Arias
Pierre Courtieu
Pierre-Marie Pédrot
Matthieu Sozeau