| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
Namely: Replacing (currently deactivated) warning on illegal ident by
an error in strict mode and nothing in soft mode.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
let-ins
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | |/ / / /
|/| | | | |
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | | |
We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | | |
Also remove obvious comments.
|
| |\ \ \ \ \ |
|
| | | | | |/
| | | |/|
| | | | |
| | | | | |
Also documenting how the implicit arguments by position are computed.
|
| | | |/ /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Instead of calling the whole reduction machirery, we check before reducing that
a term is an applied atom, i.e. inductive, constructor, evar or meta. In that
case, the abstract machine acts as the identity but needs to destruct and
reconstruct the whole term, which can be very costly.
This fixes part of bug #5421: vm_compute is very slow at doing nothing, where
recomputation of the type of a big inductive was incredibly expensive.
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | |\ \ \ \ |
|
| | | |_|/ /
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Instead of browsing the term as many times as there are abstracted constants,
we replace the constants in one pass. We have to be a bit careful to replace
the right variables though, in case there are chained abstracts. This is much
faster.
This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously
avoided by a safeguard I put in nativecode.ml. But other kernel changes
in this commit should probably be reviewed carefully.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This turned out to be costly in proofs with many abstracted lemmas, as an
important part of the time was passed in the computation of the size of the
opaquetab.
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In one case, the hashconsed type of a judgement was not used anywhere else.
In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.
|
| |\| | | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
|
| | |\| | |
|
| | |\ \ \ |
|
Maxime Dénès
Hugo Herbelin
Théo Zimmermann
Gaetan Gilbert
Pierre-Marie Pédrot
Matej Kosik
Emilio Jesus Gallego Arias