| Age | Commit message (Collapse) | Author |
|---|
|
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|
This means that all the members of the team will receive
a review request for PRs on the CI, but only one of them
will need to approve the PR, and this will remove the
review request for the others.
Currently the team contains Emilio and Gaetan, the two
former code owners of these files. It makes sense to start
experimenting on this component since they had already
decided to make their role symmetric.
Updating the list of maintainers can be done by updating
the list members, and without changing the CODEOWNER file.
|
|
|
|
|
|
|
|
|
|
|
|
Close #7617
|
|
|
|
Primary maintainers should be responsive.
[ci skip]
|
|
As per PR comment suggestion
|
|
This closes #7580
c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and
https://github.com/coq/coq/pull/7559#issuecomment-390872924. This
should be reverted if and when we move to autogenerated docs for
warnings and errors, as suggested in #7373.
|
|
To reflect reality.
[ci skip]
|
|
[ci skip]
|
|
[ci skip]
|
|
[ci skip]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Closes #7345.
[skip ci]
|
|
Mitigates #7346.
[skip ci]
|
|
|
|
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
|
|
|
|
|
|
Like CHANGES, and the test-suite folder, this file receives too many
updates to have a code owner. It is the job of the reviewer of the PR
to review changes to these files as well.
|
|
|
|
|
|
|
|
|
|
Guillaume and I agreed to switch, as the new Sphinx infrastructure
changes this component significantly.
|
|
|
|
|
|
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.
|
|
|
|
See https://help.github.com/articles/about-codeowners/ for
documentation.
|
|
Was actually pointing to https://github.com/CHANGES.
|
|
|
|
The overall goal is to reduce the number of files at the root of the repository.
|
