| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-12-12 | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau | |
| - In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed. | |||
| 2014-12-11 | Test suite: keep message in sync with actual file deletions. | Xavier Clerc | |
| 2014-12-11 | New reproduction cases for the test suite. | Xavier Clerc | |
| 2014-12-10 | Fixing orientation of postponed subtyping problems. | Hugo Herbelin | |
| In the case of conversion, postponing by preserving the initial orientation. Was wrong from its initial version in Jan 2014, but was not visible because evar-evar subtyping was approximated by evar-evar conversion. Thanks to Enrico for a very short example highlighting the problem. In particular, this fixes Ergo. | |||
| 2014-12-10 | typo | Enrico Tassi | |
| 2014-12-10 | test-suite: few tests for ".v -> .vi -> .vo" compilation chain | Enrico Tassi | |
| 2014-12-07 | Improving evar restriction (this is a risky change, as I remember a | Hugo Herbelin | |
| similar optimization broke at some time some ssreflect code; we now treat the easy case of a let-in to a rel - a pattern common in pattern-matching compilation -; later on, we shall want to investigate whether any let-in found to refer to out of scope rels or vars can be filtered out). | |||
| 2014-12-05 | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | Hugo Herbelin | |
| status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted). | |||
| 2014-12-04 | Take benefit of improved name preservation of evars in e2fa65fcc. | Hugo Herbelin | |
| 2014-12-03 | Updading test-suite. | Hugo Herbelin | |
| 2014-12-02 | When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if | Hugo Herbelin | |
| possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _). | |||
| 2014-12-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite