aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-11-10Updating test-suite after Bracketing Last Introduction Pattern set byHugo Herbelin
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-08Adapting output test inference.v after c23f0cab6 (experimentingHugo Herbelin
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-11-07Tests for syntax "Show id" and [id]:tac (shelved or not).Hugo Herbelin
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
2015-11-06Fixing complexity file f_equal.v.Hugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-11-05Add test-suite file for #4273.Matthieu Sozeau
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
2015-11-04Test file for #4397.Maxime Dénès
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Fix test suite after Matthieu's ed7af646f2e486b.Maxime Dénès
2015-10-28test cases.Gregory Malecha
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Hugo Herbelin
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-26Two test-suite files for bugs 3974 and 3975Pierre Letouzey
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Test for #4372 (anomaly in inversion in the presence of fake dependency).Hugo Herbelin
2015-10-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
2015-10-17Test for bug #4325.Pierre-Marie Pédrot
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Adding test for bug #4366.Pierre-Marie Pédrot
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-12 07:43:31 +0000