aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to c...Pierre-Marie Pédrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-24Merge PR #13455: Fix comparison of extracted array literalscoqbot-app[bot]
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction o...coqbot-app[bot]
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically a...Pierre-Marie Pédrot
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...coqbot-app[bot]
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to temp...coqbot-app[bot]
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown t...Hugo Herbelin
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefu...Pierre-Marie Pédrot
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause o...Pierre-Marie Pédrot
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
2020-10-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-22Remove test-suite/bugs/opened/bug_3395.v: not a bugGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-20 01:10:26 +0000