| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | | | | | | |
|
| | |/ / / / / / / / / /
|/| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
dependencies
|
| | | | | | | | | | | | | | | | |
|
| | |_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Since 260965d, an imperative code was semantically the identity because the
closure allocation was not performed at the right moment. Because of it
intricacy, I cannot really tell the original motivations of this piece of
code, although it looks like it was for there for pretty-printing of errors.
Anyway, both because the code was dubious and its effect not observed, it
cannot hurt to remove it.
|
| | |/ / / / / / / / / / / /
|/| | | | | | | | | | | | |
|
| |/ / / / / / / / / / / / |
|
| | |_|_|_|_|_|/ / / / /
|/| | | | | | | | | | |
|
| | |/ / / / / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
A universe substitution was lacking as the normalized evar map was dropped.
|
| | |_|_|_|/ / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | |_|_|/ / / / /
|/| | | | | | | |
|
| | |_|/ / / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
These set up PG to use the local coqtop, and the local coqlib, when
editing files in the stdlib. As per
https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use
`_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those
files. However, we cannot use it for `theories/`, because a
`_CoqProject` file will override a `.dir-locals.el` in the same
directory, and there is no way to get PG to pick up a valid `-coqlib`
from `_CoqProject` (because it'll take the path relative to the current
directory, not relative to the directory of `_CoqProject`).
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
A priori considered to be a good programming style.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
let-ins
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \
| |_|/ / / / / /
|/| | | | | | | |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
In practice, this is almost invisible except when using "refine". So,
in some sense, it is aligning the behavior of pretyping on the one of
logic.ml's "refine" so that the more natural behavior of 8.4's refine
on this issue is restored.
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
pattern-matching for refine.
|
| | |_|_|_|_|_|_|_|_|/
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
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.
|
| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|/ / / / / / / /
|/| | | | | | | | | | | |
|
| | |/ / / / / / / / / /
|/| | | | | | | | | | |
|
Maxime Dénès
Théo Zimmermann
Pierre-Marie Pédrot
Hugo Herbelin
Gaetan Gilbert
Guillaume Melquiond
Jason Gross
Matej Košík
Vadim Zaliva