| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
and 8.5/8.6 "refine"
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| | |_|_|/ /
|/| | | | |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
The addition to the test suite showcases the usage.
|
| |\ \ \ \ \ \
| |_|/ / / /
|/| | | | | |
|
| | |/ / / /
|/| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:
~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~
Thank you!
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | | |
|
| |/ / / / |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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...
|
| | |\ \ \ |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Gaetan Gilbert
Abhishek Anand (@brixpro-home)
Emilio Jesus Gallego Arias
Guillaume Melquiond
Matej Košík