| Commit message (Collapse) | Author | Age |
|
|
|
| |
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
|
| |
|
|
|
|
|
|
| |
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 was making the miniopt target fail.
|
| |\
| | |
| | |
| | | |
printer.
|
| |\ \ |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |/ / / / |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | |_|_|_|/
| |/| | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.
All error display is handled by a single, uniform path.
There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.
We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:
```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```
This commit also fixes:
- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
It was not necessary to normalize a term just to check whether it was a
global reference. The hotspot appeared in mathcomp.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
|\| | | | | | | |
|
| |\ \ \ \ \ \ \ |
|
| | |\ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
tactics.
|
| | | | | | | | | | |
|
| | |/ / / / / / / |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Bug #4957 was "unify cannot directly unify universes with evars, but can
do so indirectly".
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This commit does not modify the signature of the involved modules, only
the opaque proof terms.
One has to wonder how proofs can bitrot so much that several occurrences
of "replace 4 with 4" start appearing.
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance
difference was not conclusive enough to pay for the code ugliness.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
We do one step of loop unrolling, limit the number of allocations and
mark the function as inline.
|
| |\ \ \ \ \ \ \ \ \
| | | |/ / / / / / /
| | |/| | | | | | | |
|
| | |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Added a function that takes the first [p] elements of a vector, and
a few lemmas proving some of its properties.
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| | | |_|_|/ / / / / / / / /
| | |/| | | | | | | | | | | |
|
| | |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|