coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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...
*	Assign circleci files to @SkySkimmer, @ejgallego	Gaëtan Gilbert	2018-04-17
\|
*	Add myself as the primary maintainer of the warnings system	Maxime Dénès	2018-04-11
\|
*	Remove dev/doc/changes.md from files with a code owner.	Théo Zimmermann	2018-03-29
\| \| \| \| \| \|	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.
*	Add Michael Soegtrop as a code owner for Windows build scripts.	Théo Zimmermann	2018-03-26
\|
*	Use Pierre Corbineau GitHub nickname in CODEOWNERS.	Théo Zimmermann	2018-03-26
\|
*	Merge PR #7046: Switch maintainers for documentation	Théo Zimmermann	2018-03-23
\|\
* \|	Owners for developer tools	Maxime Dénès	2018-03-22
\| \|
\| *	Switch maintainers for documentation	Maxime Dénès	2018-03-22
\|/ \| \| \| \|	Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly.
*	Switching owners for `META.coq`	Maxime Dénès	2018-03-21
\|
*	Fix appveyor entry in CODEOWNERS.	Maxime Dénès	2018-03-21
\|
*	Refine a bit the decentralized merging process.	Maxime Dénès	2018-03-21
\| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update CODEOWNERS	Enrico	2018-03-20
\|
*	Add CODEOWNERS	Maxime Dénès	2018-03-20
\| \| \| \| \|	See https://help.github.com/articles/about-codeowners/ for documentation.
*	[PR template] Remove the relative link.	Théo Zimmermann	2018-01-05
\| \| \| \|	Was actually pointing to https://github.com/CHANGES.
*	Create pull request template.	Théo Zimmermann	2017-12-24
\|
*	Move contributing files to .github/ sub-directory.	Théo Zimmermann	2017-11-13
	The overall goal is to reduce the number of files at the root of the repository.