| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This commit proposes a fix for
https://coq.inria.fr/bugs/show_bug.cgi?id=4842
The previous feature is a bit complicated to do correctly due to the
separation over who has control of the console.
Indeed, `-timed` is a command line option of the batch compiler, so we
resort to a hack and assume control over the console. I am not very
happy with this solution but should do the job.
Note that the timing event is still being sent by the standard msg
mechanism. A particular point of interest is the duplication of paths
between the stm and vernac.
|
|
|
|
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
|
|
In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct
access to the console, recommending instead to provide information to
the user by means of the `Feedback.msg_*` facilities.
However, we introduced a display bug in the checker printer as it is
special and doesn't use the Pp facilities (likely for trust reasons),
spotted by @herbelin
This patch fixes this bug and performs a couple more of fine tunings in
the input.
However, it could be desirable to port the `checker/printer.ml` to `Pp`
and use the feedback mechanism; this would allow IDEs to use the checker
in a more convenient way, at the cost of trusting `Pp` (which is already
a bit trusted currently)
A start of that idea can be found at:
https://github.com/ejgallego/coq/tree/fix_checker_printing
|
|
|
|
|
|
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.
|
