aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
|\
| * 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
* | 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
| * | | | | 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#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| | | | |\
| | | | * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | | | |\ \
| | | | * \ \ Merge PR#752: Adding a test case as requested in bug 5205.Gravatar Maxime Dénès2017-06-15
| | | | |\ \ \
| | | | * \ \ \ Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Maxime Dénès2017-06-15
| | | | |\ \ \ \
* | | | | \ \ \ \ 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
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 01:41:41 +0000