coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\
\| *	Backtracking on interpreting toplevel calls to exact in scope determined	Hugo Herbelin	2015-10-24
\| *	Fixing a bug in reporting ill-formed inductive.	Hugo Herbelin	2015-10-22
\| *	Bug #3956 is fixed.	Matthieu Sozeau	2015-10-21
* \|	Removing test for bug #3956.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Test for #4372 (anomaly in inversion in the presence of fake dependency).	Hugo Herbelin	2015-10-19
\| *	Fixing #4198 (continued): not matching within the inner lambdas/let-ins	Hugo Herbelin	2015-10-18
\| *	Test for bug #4325.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Test file for #4346: Set is no longer of type Type	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Adding test for bug #4366.	Pierre-Marie Pédrot	2015-10-11
\| *	Fixing test-suite	Hugo Herbelin	2015-10-11
\| *	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
\| *	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin	2015-10-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Refine fix for handling of the universe contexts of hints, depending on	Matthieu Sozeau	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #4161.	Matthieu Sozeau	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07
\| *	Test for record syntax parsing.	Pierre-Marie Pédrot	2015-10-07
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
* \|	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: the stdlib now needs 5 universes	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
\| \| *	Fix test-suite file	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
\|\\|