| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | |_|/ / / /
| |/| | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
There is a long story of commits trying to improve the compatibility
between 8.4 and 8.5 refine, as discussed in
https://github.com/coq/coq/pull/346.
ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion
8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses
08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses
c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses
9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses
6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5
d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5
The current commit tries to identify (one of?) the exact points of
divergence between 8.4 and 8.5 refine, namely the types inferred for
the variables of a pattern-matching problem.
Note that for the conclusion of each new goal, there were a
nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the
compatibility expects that such a nf_betaiota on the conclusion of
each goal remains.
|
| | |\ \ \ \ \ \
| | | |_|/ / /
| | |/| | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Now it is a private field, locations are optional.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| |/ / / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| | | | | | | | |
|
| |/ / / / / / |
|
| |\| | | | | |
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | | |
Add a test-suite file to be sure we won't regress silently.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
|
| | | | | | |
|
| |\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
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...
|
| | | | |/
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows e.g. to use the record notations even when there are
defined fields.
A priori fixed also missing parameters when interpreting primitive
tokens.
|
| | |\ \ \ |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
Gaetan Gilbert
Hugo Herbelin
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Maxime Dénès
Matthieu Sozeau
Guillaume Melquiond
Matej Košík
Tej Chajed