| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |/ / / / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | | |
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
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| |\ \ \ \ \ \
| |_|/ / / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|/ / / / / / /
|/| | | | | | | | | | |
|
| | |/ / / / / / / / /
|/| | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
https://github.com/coq/coq/pull/201#discussion_r110957570
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
https://github.com/coq/coq/pull/201#discussion_r110952601
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Also move named arguments to the beginning of the functions. As per
https://github.com/coq/coq/pull/201#discussion_r110928302
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
As per Enrico's request.
|
| | | | | | | | | | | |
|
| | |_|_|_|_|_|_|_|/
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of [abstract] through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check.
It might be nice to factor it further, into a cache_term function that
caches a term, and a separate bit that calls cache_term with the result
of running the tactic.
|
| | |/ / / / / / /
|/| | | | | | |
| | | | | | | | |
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.
However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479
Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.
This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
| | |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Maxime Dénès
Jason Gross
Gaetan Gilbert
Matej Košík
Vadim Zaliva
Jason Gross
Emilio Jesus Gallego Arias