| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
between proofs in tactic injection, with a side-effect on inversion.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
This does not affect the semantics of these functions.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
|
| | | |
|
| | |
| |
| |
| | |
Order of items made stable
|
| |\ \
| | |
| | |
| | | |
Was PR#303: LtacProf cutoff is for total percent, not time
|
| |\ \ \
| | | |
| | | |
| | | |
| | | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| | | | |
| | | |
| | | |
| | | | |
Restore subst output test file modified by mistake.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#302: Set the default LtacProf cutoff to 2%
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#281: Fix indentation of -profile-ltac in -help
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#280: Document that [Reset Ltac Profile] is not synchronized with
the document state
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | |\ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#294: Make error message more helpful.
|
| |\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Was PR#257: [checker] Fix/fine tune printing.
|
| |\ \ \ \ \ \ \ \ \
| | |_|_|_|/ / / /
| |/| | | | | | | |
|
| | |\ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was PR#293: Fix #4762 (eauto weaker than auto).
|
| | | | | | | | | | | |
|
| | |_|_|_|_|_|_|_|/
|/| | | | | | | | |
|
| | |_|_|_|_|/ / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This was the original value from Tobias' code. When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information. When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want. If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
When a proof is 're-opened', the Qed node does not change.
Still the STM has to install the old state (where only
the future proof has to be updated). This bit was missing.
Why was it working: the bug happens only if you
reopen the very last proof, i.e. there is no
sentence that stays valid after the Qed. If there
is such a sentence, its state was computed correctly
before, and is not changed. If it is the very last,
then the next state is based on the wrong one...
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
It seems warnings are not taken into account in output/
tests.
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
in error messages
|
| | |_|_|_|_|_|_|_|/
|/| | | | | | | | |
|
| | | | |/ / / / / |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
| | | | | | | | | |
|
Yves Bertot
Hugo Herbelin
Pierre-Marie Pédrot
Guillaume Melquiond
Théo Zimmermann
Enrico Tassi
Maxime Dénès
Cyprien Mangin
Jason Gross
Matthieu Sozeau
Pierre Letouzey