| Commit message (Collapse) | Author | Age |
... | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can
tell.
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
See the discussion in the bug tracker, basically the STM delays the
feedback error message to a point where CoqIDE has forgotten about the
sentence, thus we were processing such errors in the generic case,
printing them twice as the Fail case will also do it.
We could indeed revert back to the 8.6 strategy for error (print
always from Fail and ignore Feedback), however I feel that time will
be better spent by fixing the STM than adding more CoqIDE workarounds.
|
|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / /
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | |_|_|_|_|/
| | | | | | | | | | | | | | | | | | | | | | | |/| | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
Undo & friends is very expensive in batch mode as backtracking state
is not kept and thus should be recomputed.
We thus warn the user.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
This was not used anywhere; it looks like dead code from some previous
attempt.
`get_hint_ctx` looks also very very suspicious.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | |
This could happen with paths on Windows, or even relative paths on all
OSs.
Fixes #5730: CoqIDE becomes unresponsive on file open.
|
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | |
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
This commit also fixes range selectors being incorrectly displayed.
|
| | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | |/ / / / / / / / / /
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
Unfortunately, some manual synchronization is needed between the
constr parser and the table of constr/pattern levels.
We do this synchronization which was missing in the commit moving
"x -> y" to a user-level notation.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
[c.f] https://coq.inria.fr/bugs/show_bug.cgi?id=4270
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
inductive types)
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
let-ins and non-recursively uniform parameters
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
(bug #4742).
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
4e70791).
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | |
The point is to emphasize stronglier when we are talking about
contexts or about arguments.
|
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
The number of effective parameters was used where the number of
declarations in the signature of parameters should have been used.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
Printing metas still happens relatively often. From the user point of
view, no need to know that it is different from an evar, so the
notation ?M42 as it was before is much lighter. As for developers
looking for debugging information, they will easily suspect that it is
internally a meta because of the "M".
This reverts "Proposing meta names more distinguishable from evar
names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
|
| | | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
The bug was caused by an inconsistency in different part of the code
for deciding where cutting the context in between recursively uniform
parameters and non-recursively uniform ones when let-ins were in the
middle. We fix it by using uniformly "context_chop".
|
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|/ / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | |
|
| | | | | |_|_|_|_|_|_|_|_|_|_|_|/ / /
| | | | |/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
Call to nf_betaiota was done on one side of the comparison preventing
the same message to be repeated twice but not on the other side.
|
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
The validity of this test depended on Makefile issueing warnings in English.
We simply force the global language of the shell to be C.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
expected.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
context obtained by ltac pattern-matching)
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|