| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
Answering to commit about #5500: we don't know in general if the
return predicate T(y1,..,yn,x) in the intermediate step of a nested
pattern-matching is a sort, but we don't even know if it is
well-typed: retyping is not enough, we need full typing.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a quick fix to check in nested pattern-matching that the
return clause is typed by an arity (there was already a check when the
return clause was given explicitly - in the 3rd section of
prepare_predicate -; it was automatically typed by a sort when the
return clause was coming by pattern-matching with the type constraint,
since the type constraint is a type; but it was not done when the
predicate was derived from a former predicate in nested
pattern-matching).
Indeed, in nested pattern-matching, we know that the return predicate
has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that
T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching
on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can
be a "match" which reduces to a sort when instantiated with v1..vn,
but whose evaluation remains blocked when the y1..yn are variables).
Note that in the bug report, the incorrect typing is produced by small
inversion. In practice, we can raise the anomaly also without small
inversion, so we fix it in the general case. See file 5500.v for
details.
|
| |\
| |
| |
| | |
AppVeyor fail.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The script now performs many more checks and reports errors in
a more intelligible way.
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
In particular, don't use the GitHub interface. Also, not all reviews are
mandatory in some corner cases.
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
too long.
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
to coq, coqchk, coqdoc
|
| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / / / /
|/| | | | | | | | | | |
|
| |/ / / / / / / / / / |
|
| |\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | | |
Sphinx doc chapter 22
|
| | |\ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / /
|/| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | | |
Sphinx doc chapter 21
|
| | |\ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / /
|/| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Sphinx doc chapter 19
|
| | |\ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / / /
|/| | | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Sphinx doc chapter 17
|
| | |_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Guillaume and I agreed to switch, as the new Sphinx infrastructure
changes this component significantly.
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Thanks to Paul Steckler for porting this chapter.
|
| | |_|_|/ / / / / / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Thanks to Pierre Letouzey for porting this chapter.
|
| | |_|/ / / / / / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Thanks to Laurent Théry for porting this chapter.
|
| | |/ / / / / / / / /
|/| | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Thanks to Clément Pit-Claudel for porting this chapter.
|
| |/ / / / / / / / / |
|
| | | | | | | | | | |
|
| |/ / / / / / / / |
|
| |\ \ \ \ \ \ \ \
| |_|_|_|/ / / /
|/| | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We make GitHub assign only principal maintainers as reviewers. This
reduces the level of noise (PRs with 10 code owners), and makes it easy
for the assignee to check if all reviews have been completed (all
reviewers in the list have to approve the PR, which was not the case
before if two reviewers were assigned for the same component).
This change means that when a principal maintainer submits a patch
touching the component they own, they should ask a review from the
secondary maintainer.
|
| |\ \ \ \ \ \ \ \
| |/ / / / / / /
|/| | | | | | | |
|
| | |_|_|/ / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Ssreflect was using a very complex function performing amongst other things
refolding to check that a term was an applied inductive type. It now relies
on a simple reduction followed by term matching.
|
| | | | | | | | |
|
| | |/ / / / /
|/| | | | | |
|
| |/ / / / / |
|
| |\ \ \ \ \ |
|
| |/ / / / / |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
The last merge with the centralized process ;)
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
See https://help.github.com/articles/about-codeowners/ for
documentation.
|
| |/ / / / / |
|
| | |/ / /
|/| | |
| | | |
| | | | |
[skip ci]
|
Hugo Herbelin
Maxime Dénès
Enrico Tassi
Théo Zimmermann
Vincent Laporte
Guillaume Melquiond
Ralf Jung
Pierre-Marie Pédrot
Enrico