coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, Z...	Emilio Jesus Gallego Arias	2018-07-01
\|\
* \	Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...	Emilio Jesus Gallego Arias	2018-07-01
\|\ \
* \ \	Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \
* \ \ \	Merge PR #7960: [build] Remove target binary before copy.	Enrico Tassi	2018-06-30
\|\ \ \ \
* \ \ \ \	Merge PR #7949: Split the Ssrmatching module between code and grammar rules.	Enrico Tassi	2018-06-30
\|\ \ \ \ \
\| * \| \| \| \|	Split the Ssrmatching module between code and grammar rules.	Pierre-Marie Pédrot	2018-06-30
\|/ / / / /
* \| \| \| \|	Merge PR #7918: Mini-update of version history with recent changes.	Théo Zimmermann	2018-06-29
\|\ \ \ \ \
\| \| \| \| \| *	Splitting primitive numeral parser/printer for positive, N, Z into three files.	Hugo Herbelin	2018-06-29
\| \| \| * \| \|	Workaround to fix #7731 (printing not splitting line at break hint).	Hugo Herbelin	2018-06-29
\| \| \| \| \|/ \| \| \| \|/\|
\| \| \| \| *	Fixes #7712 (an anomaly in reporting bad recursive notation format).	Hugo Herbelin	2018-06-29
\| \| \| \|/
* \| \| \|	Merge PR #7080: Swapping Context and Constr and defining declarations on cons...	Maxime Dénès	2018-06-29
\|\ \ \ \
\| \| \| * \|	[build] Remove target binary before copy.	Emilio Jesus Gallego Arias	2018-06-29
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #7890: Inline a function from Quote used in setoid_ring.	Maxime Dénès	2018-06-29
\|\ \ \ \
* \ \ \ \	Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retrokn...	Maxime Dénès	2018-06-29
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7950: Documentation for 8.8.1	Maxime Dénès	2018-06-29
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7860: Fix #7704: Launching coqide through PATH fails.	Emilio Jesus Gallego Arias	2018-06-28
\|\ \ \ \ \ \
\| \| * \| \| \| \|	CHANGES for 8.8.1.	Théo Zimmermann	2018-06-28
\| \| * \| \| \| \|	Self-credit for the work done.	Théo Zimmermann	2018-06-28
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7948: Syntax for naming an existential variable	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.	Michael Soegtrop	2018-06-28
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	wrong sphinx syntax	Ambroise	2018-06-28
* \| \| \| \| \| \| \|	Merge PR #7946: Update maintainers for native/VM files in pretyping	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	Update gallina-extensions.rst	Ambroise	2018-06-28
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7937: Mention Consortium in README	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	Deprecate Environ.retroknowledge function in favor of the projection	Gaëtan Gilbert	2018-06-28
\| \| \| \| \| \| * \| \| \|	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert	2018-06-28
\| \| \| \| \| \| * \| \| \|	Make Environ.globals abstract.	Gaëtan Gilbert	2018-06-28
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.	Pierre-Marie Pédrot	2018-06-28
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	Update maintainers for native/VM files in pretyping	Maxime Dénès	2018-06-28
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7934: Add mit-plv/bedrock2-ci to CI	Emilio Jesus Gallego Arias	2018-06-28
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Add mit-plv/bedrock2-ci to CI	Andres Erbsen	2018-06-27
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7939: Turn the CoqProject_file module into a pure ML file	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \|	Mention Consortium in README	Maxime Dénès	2018-06-27
\| \| \| \| \| \| \| \| \| \| * \|	Adding overlay.	Hugo Herbelin	2018-06-27
\| \| \| \| \| \| \| \| \| \| * \|	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ...	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \|	Slightly less crazy parsing algorithm for CoqProject_file.	Pierre-Marie Pédrot	2018-06-27
\| \| * \| \| \| \| \| \| \| \| \|	Turn CoqProject_file into a normal OCaml file.	Pierre-Marie Pédrot	2018-06-27
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \|	Fix 'unbound variable' issue on Windows packaging jobs.	Théo Zimmermann	2018-06-27
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \|	Test file for #7723	Maxime Dénès	2018-06-27
\| \| \| \| \| * \| \| \| \| \| \|	CoqIDE scrolls the proof buffer down to the first goal.	Cyprien Mangin	2018-06-27
\| \| \| \| \| \| \|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Fix #7723: vm_compute segfaults with universe polymorphism	Maxime Dénès	2018-06-27
\| \| \| \| \|_\|_\|/ / / / \| \| \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #7888: Clarify the message "this hint will only be used by eauto"	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft	Hugo Herbelin	2018-06-26
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7906: universes_of_constr don't include universes of monomorphic co...	Pierre-Marie Pédrot	2018-06-26
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \|