coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7082: Expliciting and taking advantage of a representation invarian...	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7184: [toplevel] Fix path initialization before vio processing (clo...	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[Sphinx] Add chapter 7	Maxime Dénès	2018-04-09
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[Sphinx] Make it possible to espace { by %{ in custom grammars	Maxime Dénès	2018-04-09
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[Sphinx] Move chapter 7 to new infrastructure	Maxime Dénès	2018-04-09
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Document requirement to have git >= 2.7 to use the merge script.	Théo Zimmermann	2018-04-08
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Merge script does not warn when the remote is set to HTTPS.	Théo Zimmermann	2018-04-08
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Merge script: use fetch URL for the remote.	Théo Zimmermann	2018-04-08
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6809: Improve shell scripts	Michael Soegtrop	2018-04-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[toplevel] Fix path initialization before vio processing (closes #7044)	Emilio Jesus Gallego Arias	2018-04-07
\| \|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Fixed many typos and grammar errors in chapter 11 of the manual.	Zeimer	2018-04-06
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...	Hugo Herbelin	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6960: [api] Move some types to their proper module.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7180: Remove unused script.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)	Enrico Tassi	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7131: Sphinx doc chapter 30	Théo Zimmermann	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Improve shell scripts	zapashcanon	2018-04-05
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6838: Light refactoring of implicit arguments	Hugo Herbelin	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Refactor impargs code.	Jasper Hugunin	2018-04-05
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove unused script.	Théo Zimmermann	2018-04-05
\| \|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.	Théo Zimmermann	2018-04-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Fix #7124: Warning "Ignoring implicit status" does not provide line number	Maxime Dénès	2018-04-05
\| \|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Fixes issue #7172 (don't include MinGW make in install)	Michael Soegtrop	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
\| \| \| \| \|_\|/ / / / / / / / / / / / / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fixing #7100 (lost of main file location in case of Ltac failure in other file).	Hugo Herbelin	2018-04-04
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \