| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ \ \ \
| |_|_|/
|/| | | |
|
| | |_|/
|/| |
| | |
| | | |
Also remove obvious comments.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
|
| | |\ \ \ |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
|
| | | | | | |
|
| | |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
It was not necessary to normalize a term just to check whether it was a
global reference. The hotspot appeared in mathcomp.
|
| | | |\ \
| |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Was breaking e.g. fiat-crypto.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
After 5db9588098f9f, some extra evar-normalization remained (compared to trunk)
that would change the semantics e.g. of change bindings under Ltac match.
This is just circumventing a fundamental flaw in the treatment of patterns.
|
| | | |\ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Instead of crawling the whole undefined evar map, we use the fold_right
function to process evars in decreasing order.
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
A lot of tactic calls actually use the open_constr_no_classes_flags option
which does not require checking anything about frozen evars. Computing it
upfront is useless in this case.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Most of the time, undefined evars are not modified by the considered function,
which leads to the costly recomputation of a trivial partition of evars. We
simply take advantage of physical equality to discriminate when this is
useless and special-case it in the type of frozen evars.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
| |\ \ \ |
|
| | | | |\
| |_|_|/
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.
We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is another perfomance-critical function in unification. Putting it in
the EConstr API was changing the heuristic, so better revert on that change.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
It seems this is a performance-critical function for unification-heavy code.
In particular, tactics relying on meta unification suffered an important
penalty after this function was rewritten with the evar-insensitive API, as
witnessed e.g. by Ncring_polynom whose compilation time increased by ~30%.
I am not sure about the specification of this function, but it seems safer
to revert the changes and just do it the old way. It may even disappear if
we get rid of the old unification algorithm at some point.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We make mli files look to what they were looking before the move to EConstr
by opening this module.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
Maxime Dénès
Gaetan Gilbert
Matej Košík
Hugo Herbelin
Pierre-Marie Pédrot
Tej Chajed