aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* test-suite/success/extraction.v : add some Extraction TestCompileGravatar Pierre Letouzey2017-07-26
* Enrich test file 4720.v with a compilation test of the extracted codeGravatar Pierre Letouzey2017-07-26
* Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Gravatar Maxime Dénès2017-07-26
|\
* \ Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \
| | * Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Gravatar Pierre Letouzey2017-07-25
| |/ |/|
| * Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
* | fake_ide: do as coqide to find out coqtop pathGravatar Enrico Tassi2017-07-20
* | more verbose logs for coq-makefileGravatar Enrico Tassi2017-07-20
* | coq-makefile: make test suite detect more errorsGravatar Enrico Tassi2017-07-20
* | Remove trailing CR before diff in output and misc tests.Gravatar Maxime Dénès2017-07-20
* | Print failure logs on appveyor.Gravatar Maxime Dénès2017-07-20
* | Remove non-terminating Timeout tests from Hints.v.Gravatar Maxime Dénès2017-07-20
* | Make coqlib relative in test suite (revert 024a7ab20b0)Gravatar Maxime Dénès2017-07-20
|/
* Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\
* \ Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \
| * \ Merge PR #745: Add timing scriptsGravatar Maxime Dénès2017-07-19
| |\ \
* | | | Getting rid of abstraction breaking code in tclABSTRACT.Gravatar Pierre-Marie Pédrot2017-07-14
* | | | Removing the uses of abstraction-breaking code in Lemmas.Gravatar Pierre-Marie Pédrot2017-07-13
* | | | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelGravatar Maxime Dénès2017-07-13
|\ \ \ \
| | | | * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| |_|_|/ |/| | |
| | * | Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
| |/ / |/| |
| * | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| * | Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| * | Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | * Add timing scriptsGravatar Jason Gross2017-07-11
| |/ |/|
* | Merge PR #863: Fixing environment in warning "Projection value has no head co...Gravatar Maxime Dénès2017-07-07
|\ \ | |/ |/|
| * Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |/ |/|
* | Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \
| * | closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
* | | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with...Gravatar Maxime Dénès2017-06-27
|\ \ \
* \ \ \ Merge PR#826: Put plugin exports in the right compatibility fileGravatar Maxime Dénès2017-06-26
|\ \ \ \
* \ \ \ \ Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\ \ \ \ \ | | |_|/ / | |/| | |
* | | | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \ \ \
| | * | | | closing bug #4250Gravatar Julien Forest2017-06-23
| |/ / / / |/| | | |
| | | | * Add tests for handling of warningsGravatar Tej Chajed2017-06-23
| | * | | Add test-suite file for funind, extraction with compat 8.6Gravatar Jason Gross2017-06-22
| |/ / / |/| | |
| | * | Should fix a false negative reported by deps-order.sh.Gravatar Hugo Herbelin2017-06-21
| |/ / |/| |
* | | Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\ \ \
* \ \ \ Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\ \ \ \
* \ \ \ \ Merge PR#760: Fixing base_include after loc is an option + a better test that...Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \
* | | | | | | Test case for bug 5578.Gravatar Maxime Dénès2017-06-19
| | | | * | | romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
* | | | | | | Increase the time limit on 4366.v to make gitlab work better.Gravatar Gaëtan Gilbert2017-06-16
| |_|_|/ / / |/| | | | |
| * | | | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| * | | | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| * | | | | Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
| * | | | | Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 23:19:29 +0000