| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
A file was introduced by mistake in theories/Logic.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
We protect the code against the presence of pattern casts where they are
not supported. Why we cannot make the pattern type reflect this is
a long story (described in this commit), but in the long term we
probably want to support them anywhere, like OCaml does. Of course, it
will require to adjust the pattern matching compiler.
|
| | |
| |
| |
| | |
Also getting rid of a global side-effect.
|
| | |
| |
| |
| |
| |
| | |
This is a bit ad-hoc, but looks better for warnings since there is
a command-line flag accepting the same values, so comma will lead to
fewer parsing issues than space.
|
| |\ \
| | |
| | |
| | |
| | | |
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#263: Fast lookup in named contexts
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#304: fixing bug 4609
|
| |/ / / /
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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 *)
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
Whether an option should be set or appended to is stored as a 2-value
flag next to the new content. This commit also cleans the code by
declaring a single object for each persistent option rather than three
different ones (one per locality).
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Yves Bertot
Théo Zimmermann
Enrico Tassi
Cyprien Mangin
Jason Gross