coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: fix test-suite file for #4287, now properly rejected.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: Remove test-suite file #3309	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix test-suite file (4301 is invalid, but a good regression test)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: correct handling of with in modules	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fixed 3685 by side-effect :)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: minor fixes to test-suite files	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix test-suite file for HoTT/coq bug #120	Matthieu Sozeau	2015-10-02
\| \| *	Univs: test-suite file for bug #2016	Matthieu Sozeau	2015-10-02
\| \| *	Univs: test-suite file for #4301, subtyping of poly parameters	Matthieu Sozeau	2015-10-02
\| \| *	Fix test-suite file for bug #3777	Matthieu Sozeau	2015-10-02
\| \| *	Fix test-suite file: failing earlier as expected.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fixed bug 2584, correct universe found for mutual inductive.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix Universe vernacular, fix bug #4287.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fixed bug #4328.	Matthieu Sozeau	2015-10-02
\| \| *	Forcing i > Set for global universes (incomplete)	Matthieu Sozeau	2015-10-02
\| \|/
\| *	Test for bug #4347.	Pierre-Marie Pédrot	2015-09-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	Test file for #3948 - Anomaly: unknown constant in Print Assumptions.	Maxime Dénès	2015-09-20
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	STM: Reset takes Ltac <ident> into account (Close #4316)	Enrico Tassi	2015-09-15
* \|	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
\| *	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin	2015-08-02
\| *	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
\| \|/
\| *	test-suite: add test for bug# 3743.	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
* \|	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
* \|	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