coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7801: [vernac] Add option to force building really mutual induction...	Enrico Tassi	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[doc] Rewrite and document the prodn directive	Clément Pit-Claudel	2018-06-19
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[doc] Fix a typo in the ssreflect chapter	Clément Pit-Claudel	2018-06-19
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[doc] Fix uncaught duplicate-label errors in the SSReflect chapter	Clément Pit-Claudel	2018-06-19
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[doc] Use productionlist instead of prodn in ring.rst	Clément Pit-Claudel	2018-06-19
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7714: Remove primitive-projection related data from the kernel	Maxime Dénès	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7856: Fix #7829: Spurious documentation failures.	Maxime Dénès	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Overlay for reference removal	Maxime Dénès	2018-06-18
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7855: Update section on adding your project to CI and link to examp...	Emilio Jesus Gallego Arias	2018-06-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Canary.	whitequark	2018-06-18
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix #7829: Spurious documentation failures.	Théo Zimmermann	2018-06-18
\| \| \| \|/ / / / / / / / / / / / / / / / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7840: Remove Hashcons.Hobj	Pierre-Marie Pédrot	2018-06-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update section on adding your project to CI and link to example PR.	Théo Zimmermann	2018-06-18
\| \|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove reference name type.	Maxime Dénès	2018-06-18
\| \|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Hashcons.Hobj.	whitequark	2018-06-17
\|/ / / / / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7848: Fix a typo in documentation	Théo Zimmermann	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7822: cArray: proper invalid_arg exceptions	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove Tutorial from Additional documentation in refman intro.	Théo Zimmermann	2018-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove Tutorials from doc/LICENSE following #7466.	Théo Zimmermann	2018-06-17
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7844: Remove Elpi from Travis.	Emilio Jesus Gallego Arias	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7828: [Spawn] no control sock on unix	Emilio Jesus Gallego Arias	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Add introduction and credits to the TOC.	Théo Zimmermann	2018-06-17
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Move indexes on top on the TOC. Closes #7764.	Théo Zimmermann	2018-06-17
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretyping	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove special declaration of primitive projections in the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7811 (uncaught Not_found in notation printer related to "match").	Hugo Herbelin	2018-06-17
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Faster and cleaner fconstr-to-constr conversion function.	Pierre-Marie Pédrot	2018-06-17
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7749: [doc] Disable smartquotes conversion	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7752: [merge script] Check if the CI that was run is outdated.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7635: Define rec_declaration in terms of prec_declaration.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Elpi from Travis.	Théo Zimmermann	2018-06-16
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7814: doc: Add "Print Canonical Projections" command to Command index	Théo Zimmermann	2018-06-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Fix #7836: tools/inferior-coq.el uses next-line instead of forward-line.	Perry E. Metzger	2018-06-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[sphinx] Finish clean-up of the Canonical Structure subsection.	Théo Zimmermann	2018-06-16
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	doc: Add "Print Canonical Projections" command to Command index	Anton Trunov	2018-06-16
\|/ / / / / / / / / / / / / / / / / /
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[spawn] don't create a control socket on Unix (Fix #7713)	Enrico Tassi	2018-06-15
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau	2018-06-15
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7813: Workaround for #2800: handling non-value arguments in tactics.	Pierre-Marie Pédrot	2018-06-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Very first try at listing the critical bugs of the history of Coq.	Hugo Herbelin	2018-06-15
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Do not allow spliting in res_pf, this is reserved for pretyping	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	evd/evarutil: safe [add_unification_pb] interface, taking EConstr's	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|