coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
\| *	Test for bug #2951.	Pierre-Marie Pédrot	2015-03-08
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix test-suite file, this is open.	Matthieu Sozeau	2015-03-03
\| \|
\| *	Add missing test-suite files and update gitignore.	Matthieu Sozeau	2015-03-03
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Fix test for #3848, still open.	Maxime Dénès	2015-02-27
\| \|
\| *	Moving test for #3467 to closed after PMP's fix.	Maxime Dénès	2015-02-27
\| \|
\| *	Fix test-suite files for bugs #2456 and #3593, still open.	Maxime Dénès	2015-02-27
\| \|
\| *	Moving tests for #2456 and #3593 to "opened" until they're fixed.	Maxime Dénès	2015-02-27
\| \|
\| *	Moving test of #3848 to "opened".	Maxime Dénès	2015-02-27
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Test for bug #3298.	Pierre-Marie Pédrot	2015-02-26
\| \|
\| *	Moving test for bug #3681 as closed.	Pierre-Marie Pédrot	2015-02-26
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-23
\|\\|
\| *	Moving test for bug #3071.	Pierre-Marie Pédrot	2015-02-21
\| \|
* \|	Removed tests for #3900 and #3944 as open bugs.	Hugo Herbelin	2015-02-21
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	Test for bug #3490.	Pierre-Marie Pédrot	2015-02-15
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-13
\|\\|
\| *	Adding test for bug #3786.	Pierre-Marie Pédrot	2015-02-11
\| \|
* \|	Several reproduction cases for the test suite.	Xavier Clerc	2015-01-28
\| \|
* \|	Several reproduction cases for the test suite.	Xavier Clerc	2015-01-28
\| \|
* \|	Revert "Update test for #3363 now that Require is forbidden inside modules."	Maxime Dénès	2015-01-18
\| \| \| \| \| \| \| \|	This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
\| *	Revert "Update test for #3363 now that Require is forbidden inside modules."	Maxime Dénès	2015-01-17
\|/ \| \| \|	This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
*	Update test for #3363 now that Require is forbidden inside modules.	Maxime Dénès	2015-01-12
\|
*	Fixing wrong notation level in #3295.	Hugo Herbelin	2014-12-19
\|
*	#3828 is solved.	Hugo Herbelin	2014-12-16
\|
*	Moving #2447 (congruence) to fixed.	Hugo Herbelin	2014-12-16
\|
*	New reproduction cases for the test suite.	Xavier Clerc	2014-12-11
\|
*	Commits on evar-evar unification fixed HoTT_coq_106 and improved the	Hugo Herbelin	2014-12-05
\| \| \| \| \|	status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
*	Adding test for bug #3417.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3487.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test of bug #3682.	Pierre-Marie Pédrot	2014-11-30
\|
*	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc	2014-11-25
\|
*	Tweak some test cases.	Xavier Clerc	2014-11-25
\|
*	Adding test for bug #3248.	Pierre-Marie Pédrot	2014-11-24
\|
*	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot	2014-11-21
\|
*	Add missing "Fail" to test case for bug #2814.	Xavier Clerc	2014-11-14
\|
*	Reproduction cases for the test suite.	Xavier Clerc	2014-11-14
\|
*	Test #3655 was failing due to an anomaly. Now it rather has to fail	Hugo Herbelin	2014-11-08
\| \| \| \|	normally, so failure is now detected by removing the "Fail".
*	Test fixed by PMP's commits from Oct 21.	Hugo Herbelin	2014-11-08
\|
*	test suite: some reproduction cases for recently-reported bugs.	Xavier Clerc	2014-11-04
\|
*	New bugs revealed fixed: #3408 by (probably) Maxime's commits	Hugo Herbelin	2014-11-03
\| \| \| \| \| \|	on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
*	More precise test for #3459.	Hugo Herbelin	2014-10-21
\|
*	Bug fixed by Hugo.	Matthieu Sozeau	2014-10-16
\|
*	Adding a timeout to bug #2447.	Pierre-Marie Pédrot	2014-10-15
\|