aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound varia...Matthieu Sozeau
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-09-06Fixing #8270 (cbn was calling zeta even when not asked for).Hugo Herbelin
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-05Merge PR #7968: Restrict universes in comInductiveGaëtan Gilbert
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
2018-09-03Merge PR #8107: Fixes #8106: anomaly if declaring levels for only printing th...Emilio Jesus Gallego Arias
2018-09-02Fixing #7867 (class error message tries to print a "fun" with no binder).Hugo Herbelin
2018-09-02Fixing #8106 (anomaly if declaring levels for only printing then only parsing).Hugo Herbelin
2018-08-31Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not Prelude.vPierre Letouzey
2018-08-28Fix #8288: cumulativity inferance ignores args to bound variablesGaëtan Gilbert
2018-08-28Fix #7795: UGraph.AlreadyDeclared with ProgramGaëtan Gilbert
2018-08-06Add regression test for issue #4202Tej Chajed
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term whic...Pierre-Marie Pédrot
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-16Restrict universes in comInductiveJasper Hugunin
2018-07-12Fix #7854: Native compilation + flambda trigger SEGFAULT.Pierre-Marie Pédrot
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-06Add test for #8004.Gaëtan Gilbert
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Matthieu Sozeau
2018-06-14Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Matthieu Sozeau
2018-06-12Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Hugo Herbelin
2018-06-12Fixes #7780 (missing lift in expanding alias under a binder in unification).Hugo Herbelin
2018-06-10Fixing #7700 (section variables bound to abbreviations were not found).Hugo Herbelin
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 03:43:34 +0000