coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add an entry to CHANGES about timing in coq_makefile	Jason Gross	2017-07-11
*	Update CHANGES with inversion_sigma entry	Jason Gross	2017-06-30
*	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\
\| *	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
* \|	Document cumulativity for inductive types	Amin Timany	2017-06-16
\|/
*	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
*	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès	2017-06-12
\|\
\| *	mention 'make world' without 'byte' in CHANGES + 2 minor suggestions	Pierre Letouzey	2017-06-01
* \|	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\ \
\| * \|	Tests for new specialize feature + CHANGES.	Pierre Courtieu	2017-05-31
\| \|/
* /	Documentation for eassert, eenough, epose proof, eset, eremember, epose.	Hugo Herbelin	2017-05-30
\|/
*	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\
* \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \
\| * \|	enters coq_makefile2	Enrico Tassi	2017-05-23
* \| \|	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\|/ /
\| *	Clarifying the interpretation path for the "constr_with_binding" argument.	Hugo Herbelin	2017-05-22
\|/
*	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\|\
* \|	Aligning on standard layout of CHANGES.	Hugo Herbelin	2017-05-13
\| *	Documenting Printing Compact Contexts + CHANGES	Pierre Courtieu	2017-05-11
* \|	Tentative note in CHANGES about now applying βι while typing "match" branches.	Hugo Herbelin	2017-04-27
\|/
*	CHANGES entry for #545.	Maxime Dénès	2017-04-19
*	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\
\| *	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot	2017-04-10
* \|	[camlpX] Enrico's changes to camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\|/
*	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\
* \|	Document the changes to IZR.	Guillaume Melquiond	2017-03-22
\| *	Farewell decl_mode	Enrico Tassi	2017-03-07
* \|	CHANGES: choice over setoids and prop. ext.	Hugo Herbelin	2017-03-03
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\
\| *	A few words in CHANGES.	Maxime Dénès	2016-12-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\|
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	[doc] Mention XML protocol on changes.	Emilio Jesus Gallego Arias	2016-11-16
\| *	Remove the list of bug fixes from CHANGES.	Maxime Dénès	2016-11-14
\| *	Update CHANGES and credits for 8.6beta1.	Maxime Dénès	2016-11-10
\| *	Mention notypeclasses refine in CHANGES	Matthieu Sozeau	2016-11-07
\| *	CHANGES for this branch.	Matthieu Sozeau	2016-11-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\
\| \| *	Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."	Maxime Dénès	2016-10-25
\| \| *	Update CHANGES.	Maxime Dénès	2016-10-25
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
* \| \|	Allocating a section in CHANGES for changes specific to 8.7.	Hugo Herbelin	2016-10-12
\| * \|	Tentatively preparing to add changes specific to v8.7 (see PR #275).	Hugo Herbelin	2016-10-12
\|/ /
* \|	Report about changes of semantics of auto as an ltac argument (see #4966).	Hugo Herbelin	2016-10-08
* \|	Remove the Set Verbose Compat option and turn the warning on by default.	Maxime Dénès	2016-10-06
* \|	Document change related to Keep Proof Equalities in CHANGES.	Maxime Dénès	2016-10-03
* \|	Being more informative about the change of behavior of "subst".	Hugo Herbelin	2016-09-29
* \|	Fix description of change in intro semantics.	Maxime Dénès	2016-09-21