aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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 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
| * | | | Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
| * | | | Correct coqchk reductionGravatar Amin Timany2017-06-16
| * | | | Disable debug printingGravatar Amin Timany2017-06-16
| * | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| * | | | Fix bugsGravatar Amin Timany2017-06-16
|/ / / /
* | | | Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \
| | | | * plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \
* | | | | | Remove dependency on -compat flag in coq_makefile test suite.Gravatar Maxime Dénès2017-06-15
| |_|_|_|/ |/| | | |
* | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
| | | | | * [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
* | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | * | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / |/| | | |
| | * | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / |/| | |
* | | | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \ \ \
* \ \ \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ | |_|_|_|/ |/| | | |
* | | | | Merge PR#757: Better sectioning on travis log printing in test-suiteGravatar Maxime Dénès2017-06-13
|\ \ \ \ \
| | | * | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |_|/ / / |/| | | |
* | | | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \ \ \
* | | | | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
* | | | | | make test-suite/save-logs.sh usable also on old MacOS XGravatar Maxime Denes2017-06-12
| | | | | * A stronger test that #use"include";; works well.Gravatar Hugo Herbelin2017-06-11
| |_|_|_|/ |/| | | |
| | * | | Fix Travis sectioningGravatar Jason Gross2017-06-10
| | * | | Better sectioning on travis log printing in test-suiteGravatar Jason Gross2017-06-09
| |/ / / |/| | |
| | | * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |_|/ |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \
* \ \ \ Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\ \ \ \
* \ \ \ \ Merge PR#600: Some factorizations of ltac interpretation functions between ss...Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \
* | | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | | | | Merge PR#691: [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 20:38:03 +0000