coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\
\| *	Update test-suite after 518049fe7.	Maxime Dénès	2015-09-03
* \|	Documenting the Shrink Abstract option.	Pierre-Marie Pédrot	2015-08-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-22
\|\\|
\| *	Fixing #4318 (anomaly when applying args to a recursive notation in patterns).	Hugo Herbelin	2015-08-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Test file for #4254: Mutual inductives with parameters on Type raises anomaly.	Maxime Dénès	2015-08-03
\| *	Continuing 817308ab (use ltac env for terms in ltac context) + fix	Hugo Herbelin	2015-08-02
\| *	Fixing test apply.v (had wrong option name).	Hugo Herbelin	2015-08-02
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Fixing test apply.v (had wrong option name).	Hugo Herbelin	2015-08-02
\| *	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin	2015-08-02
\| *	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin	2015-08-02
\| *	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
\| *	Test file for bug #4289 (buggy hash-consing of kernel name pairs	Hugo Herbelin	2015-07-30
\| *	Adding test for bug #3779.	Pierre-Marie Pédrot	2015-07-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Adding a test for bug #4280.	Pierre-Marie Pédrot	2015-07-28
\| *	Updating test-suite for #3510.	Pierre-Marie Pédrot	2015-07-28
\| *	Tests for bugs #3509 and #3510.	Pierre-Marie Pédrot	2015-07-28
\| *	Test for bug #2243.	Pierre-Marie Pédrot	2015-07-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\ \
\| \| *	Fixing #4305 (compatibility wrt 8.4 in not interpreting an	Hugo Herbelin	2015-07-27
\| \| *	Fixing bug #3736 (anomaly instead of error/warning/silence on	Hugo Herbelin	2015-07-27
\| \|/
* \|	Add an Iterative Deepening search strategy to typeclass resolution.	Matthieu Sozeau	2015-07-27
\| *	Output test for bug #2169.	Pierre-Marie Pédrot	2015-07-27
\| *	test-suite: add test for bug# 3743.	Matthieu Sozeau	2015-07-22
\| *	Extraction: fix primitive projection extraction.	Matthieu Sozeau	2015-07-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Refining 71def2f8 on too strong occur-check limiting evar-evar	Hugo Herbelin	2015-07-16
\| *	Remove old test file for #3819 (now fixed).	Maxime Dénès	2015-07-16
\| *	Fixing bug #4240 (closure_of_filter was not ensuring refinement of	Hugo Herbelin	2015-07-16
\| *	Test file for #3819.	Maxime Dénès	2015-07-16
\| *	Kernel/Checker: Cleanup fixes of substitutions due to let-ins.	Matthieu Sozeau	2015-07-09
\| *	Kernel: primitive projections handling of let-ins	Matthieu Sozeau	2015-07-09
\| *	Checker: Fix bug #4282	Matthieu Sozeau	2015-07-07
\| *	Univs: bug fix.	Matthieu Sozeau	2015-07-07
\| *	test-suite: Fix test-suite Makefile	Matthieu Sozeau	2015-07-07
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-06
\|\\|
* \|	Temporarily disable test file for #3922.	Maxime Dénès	2015-07-06
\| *	Test case for #4203, fixed by commit a51cce36.	Maxime Dénès	2015-07-06
* \|	Remove a line from test-suite.	Maxime Dénès	2015-07-02
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Notation: use same level for "@" in constr: and pattern: (Close: #4272)	Enrico Tassi	2015-07-01
* \|	Another missing Fail and comment in test-suite.	Maxime Dénès	2015-06-30
* \|	Missing "Fail" in test-suite.	Maxime Dénès	2015-06-30
* \|	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-28
\|\\|
\| *	Fix incompleteness of conversion used by evarconv	Matthieu Sozeau	2015-06-28