aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-13Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelMaxime Dénès
2017-07-12format pairs of items for pr_depth to get alternating separatorsPaul Steckler
2017-07-11Deprecate options that were introduced for compatibility with 8.5.Théo Zimmermann
2017-07-11Fix nonsensical universe abstraction in the kernel.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Add timing scriptsJason Gross
2017-07-07Merge PR #863: Fixing environment in warning "Projection value has no head co...Maxime Dénès
2017-07-07Fixing environment in warning "Projection value has no head constant".Hugo Herbelin
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-28A fix for #5598 (no discharge of Existing Classes referring to local variables).Hugo Herbelin
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with...Maxime Dénès
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-25Reorganizing functions to find the relative position of an hypothesis.Hugo Herbelin
2017-06-25Moving "assert" (internally "Cut") to the new proof engine.Hugo Herbelin
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23closing bug #4250Julien Forest
2017-06-23Add tests for handling of warningsTej Chajed
2017-06-22Add test-suite file for funind, extraction with compat 8.6Jason Gross
2017-06-21Should fix a false negative reported by deps-order.sh.Hugo Herbelin
2017-06-20Merge PR#807: romega: fix a slowdownMaxime Dénès
2017-06-19Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalMaxime Dénès
2017-06-19Merge PR#760: Fixing base_include after loc is an option + a better test that...Maxime Dénès
2017-06-19Merge PR#613: Cumulativity for inductive typesMaxime Dénès
2017-06-19Test case for bug 5578.Maxime Dénès
2017-06-18Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Hugo Herbelin
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
2017-06-16Increase the time limit on 4366.v to make gitlab work better.Gaëtan Gilbert
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Disable debug printingAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-15Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsMaxime Dénès
2017-06-15Merge PR#752: Adding a test case as requested in bug 5205.Maxime Dénès
2017-06-15Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsMaxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-15Remove dependency on -compat flag in coq_makefile test suite.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-07 15:32:35 +0000