Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.5' into trunk | 2015-03-30 | |
|\ | |||
| * | Updating test-suite (see previous commit). | 2015-03-24 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-03-11 | |
|\| | |||
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | 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. | 2015-03-08 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-03-04 | |
|\| | |||
| * | Fix test-suite file, this is open. | 2015-03-03 | |
| | | |||
| * | Add missing test-suite files and update gitignore. | 2015-03-03 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-28 | |
|\| | |||
| * | Fix test for #3848, still open. | 2015-02-27 | |
| | | |||
| * | Moving test for #3467 to closed after PMP's fix. | 2015-02-27 | |
| | | |||
| * | Fix test-suite files for bugs #2456 and #3593, still open. | 2015-02-27 | |
| | | |||
| * | Moving tests for #2456 and #3593 to "opened" until they're fixed. | 2015-02-27 | |
| | | |||
| * | Moving test of #3848 to "opened". | 2015-02-27 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-26 | |
|\| | |||
| * | Test for bug #3298. | 2015-02-26 | |
| | | |||
| * | Moving test for bug #3681 as closed. | 2015-02-26 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-23 | |
|\| | |||
| * | Moving test for bug #3071. | 2015-02-21 | |
| | | |||
* | | Removed tests for #3900 and #3944 as open bugs. | 2015-02-21 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-15 | |
|\| | |||
| * | Test for bug #3490. | 2015-02-15 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-13 | |
|\| | |||
| * | Adding test for bug #3786. | 2015-02-11 | |
| | | |||
* | | Several reproduction cases for the test suite. | 2015-01-28 | |
| | | |||
* | | Several reproduction cases for the test suite. | 2015-01-28 | |
| | | |||
* | | Revert "Update test for #3363 now that Require is forbidden inside modules." | 2015-01-18 | |
| | | | | | | | | This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | ||
| * | Revert "Update test for #3363 now that Require is forbidden inside modules." | 2015-01-17 | |
|/ | | | | This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | ||
* | Update test for #3363 now that Require is forbidden inside modules. | 2015-01-12 | |
| | |||
* | Fixing wrong notation level in #3295. | 2014-12-19 | |
| | |||
* | #3828 is solved. | 2014-12-16 | |
| | |||
* | Moving #2447 (congruence) to fixed. | 2014-12-16 | |
| | |||
* | New reproduction cases for the test suite. | 2014-12-11 | |
| | |||
* | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | 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. | 2014-11-30 | |
| | |||
* | Test for bug #3487. | 2014-11-30 | |
| | |||
* | Test of bug #3682. | 2014-11-30 | |
| | |||
* | Bug #3804 is actually closed (thanks to Jason Gross for the notification). | 2014-11-25 | |
| | |||
* | Tweak some test cases. | 2014-11-25 | |
| | |||
* | Adding test for bug #3248. | 2014-11-24 | |
| | |||
* | Cleaning up closed bugs in test-suite. | 2014-11-21 | |
| | |||
* | Add missing "Fail" to test case for bug #2814. | 2014-11-14 | |
| | |||
* | Reproduction cases for the test suite. | 2014-11-14 | |
| | |||
* | Test #3655 was failing due to an anomaly. Now it rather has to fail | 2014-11-08 | |
| | | | | normally, so failure is now detected by removing the "Fail". | ||
* | Test fixed by PMP's commits from Oct 21. | 2014-11-08 | |
| | |||
* | test suite: some reproduction cases for recently-reported bugs. | 2014-11-04 | |
| | |||
* | New bugs revealed fixed: #3408 by (probably) Maxime's commits | 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. | 2014-10-21 | |
| | |||
* | Bug fixed by Hugo. | 2014-10-16 | |
| | |||
* | Adding a timeout to bug #2447. | 2014-10-15 | |
| |