aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-06-25Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.Pierre-Marie Pédrot
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ...Maxime Dénès
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-05-28Fix #10264: Singleton class field data is erroneous.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-21Fixing a small bug in computing implicit arguments in (co-)fixpoints.Hugo Herbelin
2019-05-21Adding test for old bug fixed in 8.5 (wrong implicit arguments in fixpoint).Hugo Herbelin
2019-05-20Merge PR #9530: Remove `VtUnkown` classificationGaëtan Gilbert
2019-05-20Merge PR #9873: Remove test file with Timeout that failed spuriously.Gaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-16Fix #10176: shadowing vs automatic class based generalizationGaëtan Gilbert
2019-05-14Fix #10161: occur check when defining an algebraic universe.Gaëtan Gilbert
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...Maxime Dénès
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...Pierre-Marie Pédrot
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-05-03Fix #9994: `revert dependent` is extremely slow.Pierre-Marie Pédrot
2019-05-02Test case for #5752Maxime Dénès
2019-04-29Fix variant of #9344 for native_computeMaxime Dénès
2019-04-29Fix #9344, #9348: incorrect unsafe to_constr in vnormGaëtan Gilbert
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-03-31Remove test file with Timeout that failed spuriously.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-27Merge PR #9837: Fix some critical-bugs informationsThéo Zimmermann
2019-03-26Fix reproduction info for some past critical bugsGaëtan Gilbert
2019-03-26[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)Enrico Tassi
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:14:07 +0000