coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix #5539: algebraic universe produced by cases.	Gaëtan Gilbert	2018-04-06
*	Merge PR #7131: Sphinx doc chapter 30	Théo Zimmermann	2018-04-06
\|\
* \	Merge PR #6838: Light refactoring of implicit arguments	Hugo Herbelin	2018-04-05
\|\ \
* \| \|	Refactor impargs code.	Jasper Hugunin	2018-04-05
* \| \|	Merge PR #7169: Sphinx docs: fix typo in Chrząszcz (non-ASCII character lost...	Maxime Dénès	2018-04-05
\|\ \ \
* \ \ \	Merge PR #7074: Update merging doc	Maxime Dénès	2018-04-05
\|\ \ \ \
\| * \| \| \|	Add note for homebrew users.	Théo Zimmermann	2018-04-05
\| * \| \| \|	Some advice about merge script dependencies.	Théo Zimmermann	2018-04-05
\| * \| \| \|	Improve the MERGING doc.	Théo Zimmermann	2018-04-05
\| * \| \| \|	Adapt CONTRIBUTING to recent changes in Coq.	Théo Zimmermann	2018-04-05
\|/ / / /
* \| \| \|	Merge PR #7115: Sphinx doc chapter 28	Théo Zimmermann	2018-04-05
\|\ \ \ \
* \ \ \ \	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \
\| \| \| \| \| \| *	[Sphinx] Add chapter 30	Maxime Dénès	2018-04-05
\| \| \| \| \| \| *	[Sphinx] Move chapter 30 to new infrastructure	Maxime Dénès	2018-04-05
\| \| \| \| \|_\|/ \| \| \| \|/\| \|
* \| \| \| \| \|	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7163: merge-pr.sh: cache github API calls	Maxime Dénès	2018-04-04
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	Sphinx docs: fix typo (non-ASCII character lost in sphinx migration)	Peter LeFanu Lumsdaine	2018-04-04
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	[Sphinx] Add chapter 28	Maxime Dénès	2018-04-04
\| \| \| \| \| * \|	[Sphinx] Move chapter 28 to new infrastructure	Maxime Dénès	2018-04-04
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7158: [meta] Add `num` to the set of base libraries.	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6407: Fix #6404 - Print tactics called by ML tactics	Pierre-Marie Pédrot	2018-04-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7147: [doc] Document better ocamlfind and flambda requirements.	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps with...	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7104: Sphinx doc chapter 27	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7048: Sphinx doc chapter 25	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7049: Sphinx doc chapter 26	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7047: Sphinx doc chapter 24	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7041: Sphinx doc chapter 23	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7037: Sphinx doc chapter 18	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	merge-pr.sh: cache github API calls	Gaëtan Gilbert	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7154: Update coq_makefile timing test	Gaëtan Gilbert	2018-04-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Document better ocamlfind and flambda requirements.	Emilio Jesus Gallego Arias	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[meta] Add `num` to the set of base libraries.	Emilio Jesus Gallego Arias	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Update coq_makefile timing test	Jason Gross	2018-04-02
\|/ / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| * / / / /	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...	Pierre-Marie Pédrot	2018-04-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7132: [doc] Add some more documentation to STM API.	Enrico Tassi	2018-04-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6802: Remove deprecated commands Implicit Arguments and Arguments S...	Enrico Tassi	2018-04-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[toplevel] Protect goal printing better wrt Break [fixes #7142]	Emilio Jesus Gallego Arias	2018-04-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[stm] More cleanup of "classification is not an interpreter"	Emilio Jesus Gallego Arias	2018-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias	2018-04-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \|	[doc] Add some more documentation to STM API.	Emilio Jesus Gallego Arias	2018-03-31
\| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Add CHANGES for removing Implicit Arguments and Arguments Scope	Jasper Hugunin	2018-03-30
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Remove deprecated commands Arguments Scope and Implicit Arguments	Jasper Hugunin	2018-03-30
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7121: Remove outdated patch from ci-sf	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \