aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
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
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the tes...Martin Bodin
2020-08-18Fix subject reduction VS cumulative inductives and function etaGaëtan Gilbert
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
2020-06-08Fix 12483Pierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 19:39:44 +0000