| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
| |\| | | | |
|
| | | |/ /
| |/| | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
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.
|
| | |\ \ \ \ \
| | | |_|_|/
| | |/| | | |
|
| |\| | | | | |
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | |
| | | | | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This patch converts the `search_*` functions to use an iter-style API.
Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.
It also allows different printers to be used.
I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).
As a minor tweak, we make search with "Output Name Only" more efficient.
Motivation:
-----------
Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:
```ocaml
val generic_search : int option -> display_function -> unit
```
This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.
The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.
However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.
|
| | | |_|/
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
It was not very useful as just parsing won't get you very far due to
lack of notation loading.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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/`.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Also renaming vernac_com into interp_vernac and eval_expr into
process_vernac to clarify that it does side-effects (on the contrary
of Stm.interp/Vernacentries.interp).
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Moving set_formatter_out_channel where it naturally closes the
corresponding opening set_formatter_output_functions.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is not fully satisfactory though since we would not like to have
"eval_expr" depending on a parsing/lexing/comments state... but it
does because of eval_expr possibly printing the vernac expression
given to it.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
| |\| | | |
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | | |
We simply explicit that the type is actually referring to the return type,
not to the type of the argument of the pattern-matching. Note that the
heuristic could be enhanced so as to use the same code in both let-style
and match-style pattern-matching, but I'm leaving this for another time.
|
| | |\ \ |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.
(Not to be pushed to v8.6 which has a better fix).
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
| | | | | |
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This option was not doing anything... Today, one can turn the
compatibility notations warning into an error, if ever that was the
intended semantics.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
These warnings can now be configured like any other, so we don't need
a specific option anymore.
|
| |\| | | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Objects registered through the callback functions were pushed on the libstack
before the ML-MODULE object itself, leading to anomalies when the corresponding
object was assuming that the ML module was properly defined in any other Coq
module requiring the Declare ML command.
|
| | | | |
| | | |
| | | |
| | | | |
Also getting rid of a global side-effect.
|
| | |\ \ \
| | | | |
| | | | |
| | | | |
| | | | | |
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
| | | | | | |
|
| |\| | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The blacklist set was converted into a string list for each item in the
environment during a search. In fact, the blacklist was checked for
each item, even if the item was already known to be ultimately discarded.
This commit fixes both performance issues. First, blacklist_filter is no
longer used directly but in two stages. Second, the boolean values are
no longer computed before calling the shortcutting operators. It seems
like someone had already noticed part of the second issue, since some (but
not all) of the boolean values were lazily computed.
The speed up becomes noticeable when the blacklist set contains more than
four elements.
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#281: Fix indentation of -profile-ltac in -help
|
Matthieu Sozeau
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Emilio Jesus Gallego Arias
Guillaume Melquiond