| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
| | |
| | |
| | |
| | | |
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
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.
We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.
Test suite passes.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
in error messages
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
| |/ / /
| | |
| | |
| | |
| | |
| | | |
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
It seems that such options were adding the considered path to the ML loadpath
as well, which is not what is documented, and does not provide an atomic way
to manipulate Coq loadpaths.
|
| | | |
| | |
| | |
| | |
| | | |
All compilation (by)products are placed where -o specifies.
Used to be the case for .vo, .vio, .aux but not .glob
|
| | | | |
|
| |/ / |
|
| | |
| |
| |
| | |
This way par:eauto and all:eato print the same debugging traecs
|
| | |
| |
| |
| | |
not exist.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When Mltop.add_rec_path was called to add paths to the loadpath, it was
also adding the top directory to the mlpath. In particular, "theories" was
added to the mlpath although it was explicitly marked "~with_ml:false".
The "plugins" and "user-contribs" subdirectories were scanned twice, once
for filling the loadpath and then for filling the mlpath.
This patch adds an argument to Mltop.add_rec_path to explicitly control
which paths from the loadpath are added to the mlpath (none, the top one,
all of them). The "top" option was the single old behavior; the "none"
option is used for "theories"; the "all" option is used to avoid
duplicate scanning for "plugins" and "user-contribs".
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The number of path canonizations was quadratic in the number of potential
plugin directories. This patch makes it linear; on a standard Coq tree,
this brings the number of chdir and getcwd system calls from more than
1,000 down to about 200 at startup.
This also fixes a bug where the Cd vernacular command could cause plugins
to break since relative paths were used to locate them.
|
| | | |
|
| | | |
|
| | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Enrico Tassi
Emilio Jesus Gallego Arias
Matthieu Sozeau
Yves Bertot
Jason Gross