| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
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.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
| | |\ \
| | | |
| | | |
| | | |
| | | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
It seems warnings are not taken into account in output/
tests.
|
| | |/ / |
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre Courtieu
Pierre-Marie Pédrot
Guillaume Melquiond
Maxime Dénès
Matthieu Sozeau
Enrico Tassi