| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 0d364f7aa5cee042f0b327966fce35778f3285e0.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit e180cce2384bacaa5ad5b9d6e15b55de8cc913cc.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 28973285f4b9389ed0610b94ba907684214dd279.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
off by default
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We use heaps instead of continuously adding elements to an ordered list,
which was quadratic in the worst case.
As a byproduct, this solves bug #5359, which was due to a stack overflow on
big lists.
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Several cleanups were performed.
1. Removal of dead code lurking around.
2. Removal of global variables used to pass arguments to functions, as well as
unnecessary mutable state here and there. We rely on state-passing and
encapsulated mutable state.
3. Removal of crazy reference manipulation and its replacement with proper list
handling, as well as cleaning up the source and taking advantage of invariants.
This should solve algorithmic limitations of the previous code.
4. Opacification of some structures to have a clearer idea of the code
requirements.
5. Cleaning of debug printing functions. We thunk the computation of the
debugging data, whose computation can be costly for no reason, and we rely
on Feedback-based interaction instead of Printf-debugging.
|
| |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
8e07227c5853de78eaed4577eefe908fb84507c0 introduced an
incorrect duplicate of `position_error_tag_at_sentence`, which
sets the end of the underlining position starting at the end of the
sentence, whereas the location in the feedback refers to the
beginning, thus it highlights more text than it should.
This was missed in 8.6 as it seems that the code was not called.
We undo the duplication and fix the bug.
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
|
|\ \ \ \ \ \ |
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This fixes the bug in `Drop` reported by @mattam82: after performing a
`Drop`, the feeder was lost and no further message from Coq was
printed.
|
| | | | | | |
|
| | | | | | |
|
|\ \ \ \ \ \ |
|
| | | | |\ \ \
| |_|_|_|/ / /
|/| | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This was making the miniopt target fail.
|
| | | | | | | |
|
| |_|/ / / /
|/| | | | | |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
|
| |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
printer.
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|