| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
This reverts commit 5358515f23d1cd47d4914c55dcf049df858b9dc7.
The syntax is deprecated in 8.6, so we now remove it from trunk.
|
| |\ |
|
| | |
| |
| |
| |
| | |
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
|
| |\| |
|
| | |\
| | |
| | |
| | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| | |\ \
| | | |
| | | |
| | | | |
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.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
| | | | |
| | | |
| | | |
| | | | |
This is useful for debugging purposes.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | | |
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
This covers the case e.g. of "xₚ" (until the table of unicode
characters is upgraded!).
|
| | | |
| | |
| | |
| | |
| | | |
`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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/`.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
|
| | |/ |
|
| |\| |
|
| | |
| |
| |
| |
| | |
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
the state of parsable streams, so that different lexing/parsing
processes can be started independently without conflicting.
Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.
Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).
In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| | |
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
|
| | |\
| | |
| | |
| | |
| | | |
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
That way, bullet detection no longer depends on a global variable
indicating whether a line is starting. This causes a small change in the
recognized language. Before the commit, "--++" was recognized as a bullet
"--" followed by a keyword "++" when at the start of a line; now it is
always recognized as a keyword "--++".
This also fixes a bug in Tok.to_string as a side-effect.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |/ |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
One of them revealed a true bug.
|
| |\ \
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ / |
|
| |\ \
| |/
|/| |
|
| | |
| |
| |
| |
| |
| | |
They were mostly useless, and people complained about it. Not that because
there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit
out its share of noisy warnings.
|
| | | |
|
| | | |
|
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau