| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was an overlook. There was no reason to let it in the tactics/ folder,
as is was semantically part of the Ltac implementation.
|
| | | | | |
|
| |_|_|/
|/| | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where
we got a few cases wrong wrt to newline endings.
Thanks to @herbelin for pointing it out.
This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The logic was backward: if the path of a symbol was a prefix of the
current path, then the current path (without sections) was used. But what
we want is that, if the current path (without sections) is a prefix of the
path of a symbol, then the former should be used.
This fixes about 1,600 broken links in the documentation of the standard
library.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
|\ \ \ \ \ |
|
|/ / / / / |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
when the rewrite lemma doesn't typecheck or does not
correspond to a relation.
|
| | | | |
| | | | |
| | | | |
| | | | | |
Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Option Standard Proposition Elimination Scheme from 8.5 was not
documented in the right section.
|
|/ / / / |
|
|/ / / |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Moreover, this commit makes sure that an empty line after a list is always
translated into a break. ("StartLevel 1" was excluded, for some reason.)
It also avoids some code duplication. In particular, "stop_item ()" is
defined as "reach_item_level 0", so there is no reason to handle
"StartLevel 1" specially.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \
| | |_|_|/
| |/| | | |
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
| | |\ \ \ \ |
|
| | |/ / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".
In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed.
I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
While the performance gain should go unnoticed in most cases, in some
degenerate situations, e.g. the evar-stressing test-case of bug #4964,
this commit speeds up coq by 10% since most of the time is spent scanning
long lists with most of the elements filtered out.
Note that this commit also changes the scanning order to front-to-back,
which is a bit less surprising (though no code should ever depend on the
scanning order).
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This saves a quadratic allocation by replacing arrays with maps.
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
| | | | | | |
|
|/ / / / / |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
Modulo delta for types should be fully transparent.
|
|\| | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
|