| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | |
|
| | | | | | | | |
|
| | |\ \ \ \ \ \ |
|
| | |/ / / / / / |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
| | |/ / / / / |
|
| |\| | | | | |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
"Context.Rel.Declaration.to_tuple" function"
This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200.
While the of_tuple function is clearly dubious and mostly used for compatiblity reasons,
and thus had to be removed, I think that the to_tuple function is still useful as it
allows to access each component of the declaration piecewise. Without it, some codes
tend to get cluttered with useless projections here and there.
|
| | |/ / / |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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".
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
function
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
function
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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
|
| | | | | | | |
|
Pierre-Marie Pédrot
Paul Steckler
Matthieu Sozeau
Hugo Herbelin
Enrico Tassi
Guillaume Melquiond
Xavier Leroy
Matej Kosik
Matthieu Sozeau