coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...	Pierre-Marie Pédrot	2015-05-18
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
* \|	#3953 now closed.	Hugo Herbelin	2015-05-14
\| *	Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).	Hugo Herbelin	2015-05-09
\| *	Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for	Hugo Herbelin	2015-05-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Updating test-suite (see previous commit).	Hugo Herbelin	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| *	Test for bug #2951.	Pierre-Marie Pédrot	2015-03-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|