| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-12 | Fixed test-suite file, that should always work. | Matthieu Sozeau | |
| 2015-02-12 | Add test-suite files for closed bugs. | Matthieu Sozeau | |
| 2015-02-12 | COMPATIBILITY: add note about the change of behavior of Instance foo := | Matthieu Sozeau | |
| {| |}. Add test-suite files for closed bugs. | |||
| 2015-02-12 | Univs: fix bug #4031: wrong folding of sigma in change. | Matthieu Sozeau | |
| 2015-02-11 | Adding test for bug #3786. | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding a test-suite for tactic notation naming. | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding test for bug #3900. | Pierre-Marie Pédrot | |
| 2015-02-10 | Fixing #4001 (missing type constraints when building return clause of match). | Hugo Herbelin | |
| 2015-02-10 | Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵ | Hugo Herbelin | |
| declarations). | |||
| 2015-02-10 | Fixing #4018 (uncaught exception on non-equality in intros [=]). | Hugo Herbelin | |
| 2015-02-10 | Test for bug #4012. | Pierre-Marie Pédrot | |
| 2015-01-25 | Test for bug #3798. | Pierre-Marie Pédrot | |
| 2015-01-18 | There was one more universe needed due to the use of now ↵ | Matthieu Sozeau | |
| non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again. | |||
| 2015-01-17 | Back to 4 expected universes. | Matthieu Sozeau | |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-17 | Revert "Adapting two files from test-suite to now forbidden Require's in ↵ | Maxime Dénès | |
| modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e. | |||
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
| 2015-01-17 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès | |
| This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda. | |||
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau | |
| match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes. | |||
| 2015-01-16 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau | |
| Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73. | |||
| 2015-01-13 | TCs: Properly handle Hint Extern with conclusions of the form _ -> _ | Matthieu Sozeau | |
| in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794. | |||
| 2015-01-13 | Fix test-suite file, we were testing that no anomaly was raised | Matthieu Sozeau | |
| and this is the case now. | |||
| 2015-01-12 | Fix files in test-suite having to do with Require inside modules. | Maxime Dénès | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-12 | Update test for #3363 now that Require is forbidden inside modules. | Maxime Dénès | |
| 2015-01-12 | Fixing name of evars in output test Notation.v. | Hugo Herbelin | |
| 2015-01-11 | Extraction: discard code unnecessary to fulfill a module signature | Pierre Letouzey | |
| 2015-01-09 | STM: fix handling of side effects in vio2vo | Enrico Tassi | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Fixing test for bug #2830. | Pierre-Marie Pédrot | |
| 2015-01-05 | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau | |
| Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection. | |||
| 2015-01-04 | Adapting two files from test-suite to now forbidden Require's in modules. | Hugo Herbelin | |
| Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?). | |||
| 2015-01-03 | Fixing #3896 (incorrect sigma given to printer). | Hugo Herbelin | |
| 2015-01-03 | Fixing #3895 (thanks to PMP for diagnosis). | Hugo Herbelin | |
| 2015-01-01 | An optimization in the use of unification candidates so as to get the | Hugo Herbelin | |
| following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a. | |||
| 2014-12-30 | Fixing #3892: Ensure that notation variables do not capture names | Hugo Herbelin | |
| hidden behind another notation. | |||
| 2014-12-27 | include test-suite/coqchk in the summary log | Enrico Tassi | |
| 2014-12-26 | new test for coqchk | Enrico Tassi | |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi | |
| 2014-12-19 | Fixing wrong notation level in #3295. | Hugo Herbelin | |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi | |
| 2014-12-17 | Future: blocking by default | Enrico Tassi | |
| This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script. | |||
| 2014-12-16 | #3828 is solved. | Hugo Herbelin | |
| 2014-12-16 | Moving #2447 (congruence) to fixed. | Hugo Herbelin | |
| 2014-12-16 | Test for #3654. | Hugo Herbelin | |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau | |
| 2014-12-15 | Adapted test file for About. | Pierre Courtieu | |
| 2014-12-15 | Tests for #3848 and #3854. | Hugo Herbelin | |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 2014-12-15 | Tests for Searchxxx commands added and modified. | Pierre Courtieu | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite