| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-28 | Fixing #3293 (eta-expansion at "match" printing time was failing | Hugo Herbelin | |
| because of let-in's interpreted as being part of the expansion). | |||
| 2014-04-22 | Add regression tests for 3188 and 3265 | Jason Gross | |
| 2014-04-20 | Adding a test for bug #2923. | Pierre-Marie Pédrot | |
| 2014-04-20 | Adding a test for bug #3285. | Pierre-Marie Pédrot | |
| 2014-04-10 | better description of bug 3251 | Enrico Tassi | |
| 2014-04-10 | coqtop -batch refuses Back 1 but accepts Undo. | Pierre Boutillier | |
| 2014-04-10 | By resolution of the CoqWG, instantiate must not be used now that refine works | Pierre Boutillier | |
| 2014-04-10 | No more Coersion in Init. | Pierre Boutillier | |
| 2014-04-10 | Define [projT3] and [proj3_sig] | Jason Gross | |
| Also allow [projT1]/[projT2] to work for [sigT2]s and [proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions. This closes Bug 3044. This closes Pull Request #4. | |||
| 2014-04-10 | Test case for bug 3037 | Jason Gross | |
| Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9 | |||
| 2014-04-10 | Test case for 3164 | Jason Gross | |
| Closed in 69c4d0fd7b8325187e8da697a9c283594047d. I used [Timeout 2] to distinguish between stack overflow and immediate return. | |||
| 2014-04-10 | Test case for bug 3262 | Jason Gross | |
| Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough. | |||
| 2014-04-10 | Test case for bug #3217 | Jason Gross | |
| It was fixed in c3feef4ed5dec126f1144dec91eee9c0f0522a94. The test case uses [Timeout 2] to test for "Coq runs instantaneously rather than running out of memory". Hopefully this is robust enough. | |||
| 2014-04-10 | Add a regression test for bug 3001 | Jason Gross | |
| 2014-04-09 | Add another critical bug to the test-suite. | Maxime Dénès | |
| I have a fix, I'm reviewing it because there may be other bugs around. | |||
| 2014-04-09 | Adapt test-suite to -I is ML only | Pierre Boutillier | |
| 2014-04-05 | Test for bug #3142, actually duplicate of #3262. | Hugo Herbelin | |
| 2014-04-05 | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | |
| 2014-04-04 | Remove option -g as it is non-portable yet does not have any effect on the ↵ | Guillaume Melquiond | |
| test-suite. (Fix for bug #3024) | |||
| 2014-04-02 | Add a test case for bug 3251 | Jason Gross | |
| It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca. | |||
| 2014-04-01 | Fixing bug #2900 (evar/evar unif was supposed to be treated in | Hugo Herbelin | |
| solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress). | |||
| 2014-03-26 | test for apply + TC resolution | Enrico Tassi | |
| 2014-03-13 | nanoPG: better copy/paste | Enrico Tassi | |
| 2014-03-01 | Never suppress the typing constraint of bound variables whose name was | Pierre-Marie Pédrot | |
| reserved with Implicit Type. | |||
| 2014-02-28 | Pos.compare_cont takes the comparison as first argument | Pierre Boutillier | |
| Helps cbn tactic refolding | |||
| 2014-02-28 | test-suite: opaque term -> opaque proof | Pierre Boutillier | |
| 2014-02-28 | test-suite: New names for vars but the expected invariant is preserved | Pierre Boutillier | |
| 2014-02-28 | Fix output test-suite 'simpl tactic' -> 'reduction tactics' | Pierre Boutillier | |
| 2014-02-10 | fake_ide: ported to spawn | Enrico Tassi | |
| 2014-01-25 | Adding a test for bug #3023. | Pierre-Marie Pédrot | |
| 2014-01-15 | Test case containing a proof of false due to a DeBruijn off-by-one error in the | Maxime Dénès | |
| code checking allowed sorts for elimination. | |||
| 2014-01-13 | rename Paral-ITP demo file | Enrico Tassi | |
| 2014-01-13 | Paral-ITP demo: better comments | Enrico Tassi | |
| 2014-01-13 | STM: fix very simple demo | Enrico Tassi | |
| 2014-01-10 | Fix bug#2080: error message on Ltac name clash with primitive tactics | xclerc | |
| 2014-01-06 | fix simple test for paral-itp | Enrico Tassi | |
| 2014-01-06 | Add a test suite file for Ltac's "+" tactical. | Arnaud Spiwack | |
| 2013-12-21 | Test case for the buggy commutative cut subterm rule. | Maxime Dénès | |
| 2013-12-20 | micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵ | Frédéric Besson | |
| and nia. | |||
| 2013-12-19 | test-suite/output/Notations : evar number change | Pierre Boutillier | |
| 2013-12-19 | Missing Fail in r16792 | Pierre Boutillier | |
| 2013-12-17 | test guard condition against feature incompatible with prop-ext | Bruno Barras | |
| 2013-12-17 | Tentative fix of the guardedness checker by Christine and me. All stdlib and ↵ | Matthieu Sozeau | |
| test-suite pass. | |||
| 2013-12-16 | Added test-suite for bug #2990. | Pierre-Marie Pédrot | |
| 2013-12-12 | Better unification for [projT1] and [proj1_sig]. | Jason Gross | |
| This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies with [fun A (P : A -> Prop) (X : sigT P) => projT1 X]. This closes Bug 3043. | |||
| 2013-12-06 | Remove duplicate test-suite file. | Arnaud Spiwack | |
| success/instantiate.v was a duplicate of bugs/closed/1041.v | |||
| 2013-12-06 | Fix the refine related test-suite files to account for the new refine. | Arnaud Spiwack | |
| 2013-12-02 | Test case for bug#2848. | xclerc | |
| 2013-12-02 | Test suite: update output reference. | xclerc | |
| 2013-12-02 | Print logical name rather than path (thus allowing reproducible tests). | xclerc | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite