aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under l...Pierre-Marie Pédrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
2020-10-08Check complexity of primitive arrays.Guillaume Melquiond
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
2020-10-02setoid_rewrite: record generated name when rewriting under lambdaGaëtan Gilbert
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...Pierre-Marie Pédrot
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
2020-08-31Fix mangle names issue in inductionGaëtan Gilbert
2020-08-29Merge PR #12929: Make abstract compatible with mangle namesPierre-Marie Pédrot
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
2020-08-28Add test for past anomalyGaëtan Gilbert
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its documenta...Hugo Herbelin
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 01:17:13 +0000