coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...	Jason Gross	2018-04-12
\|\
* \|	Fix the status of some resolved bugs	Tej Chajed	2018-04-11
\| *	Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.	Théo Zimmermann	2018-04-05
\|/
*	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
*	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
*	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\
* \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| *	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias	2018-03-03
\|/
*	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
*	Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction	Jasper Hugunin	2018-01-17
*	Using is_conv rather than eq_constr to find `nat` or `Z` in omega.	Hugo Herbelin	2017-11-23
*	Move bug files to match their new GitHub ID (fixes #6001).	Théo Zimmermann	2017-10-23
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
*	remove unneeded -emacs flag to coq-prog-args	Paul Steckler	2017-05-01
*	Merge commit '633ed9c' into v8.6	Maxime Dénès	2016-11-17
\|\
\| *	Add test suite files for 4700-4785	Jason Gross	2016-11-17
* \|	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
* \|	Arguments: cleanup + detect discrepancy rename/implicit (#3753)	Enrico Tassi	2016-09-29
* \|	Marking bug #3383 as solved.	Pierre-Marie Pédrot	2016-07-18
* \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\ \ \| \|/ \|/\|
* \|	Fix test-suite for opened bug #4813.	Pierre-Marie Pédrot	2016-06-15
* \|	For the record, an example one would like to see working.	Hugo Herbelin	2016-06-12
\| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	2016-06-09
* \|	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
* \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fixing #4256 and #4484 (changes in evar-evar resolution made that new	Hugo Herbelin	2016-01-12
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Now closed.	Matthieu Sozeau	2015-11-11
* \|	Removing test for bug #3956.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Univs: fixed 3685 by side-effect :)	Matthieu Sozeau	2015-10-02
\| *	Univs: fix test-suite file for HoTT/coq bug #120	Matthieu Sozeau	2015-10-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Tests for bugs #3509 and #3510.	Pierre-Marie Pédrot	2015-07-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Remove old test file for #3819 (now fixed).	Maxime Dénès	2015-07-16
* \|	Temporarily disable test file for #3922.	Maxime Dénès	2015-07-06
* \|	Fix test file for #4214 which was fixed by Hugo.	Maxime Dénès	2015-06-29
* \|	Better test case by PMP for #3948.	Maxime Dénès	2015-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	Removing test for opened bugs that were already present in the closed test-su...	Pierre-Marie Pédrot	2015-05-18