aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
2019-11-05Fixing test-suiteKenji Maillard
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-10-31Fix #8459: anomaly not enough abstractions in fix bodyGaëtan Gilbert
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-28Fix #10903: type-in-type allows fixpoints on sprop inductivesGaëtan Gilbert
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of introp...Pierre-Marie Pédrot
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in #...Hugo Herbelin
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-07-29Add a test for #10088.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 12:33:51 +0000