aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...coqbot-app[bot]
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Add tests for implicit argumentsPierre Roux
2020-11-05[numeral notation] RPierre Roux
2020-11-05[numeral notation] QPierre Roux
2020-11-04[numeral notation] Add tests for the via ... using ... optionPierre Roux
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
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-03Fix test-suite in async mode.Théo Zimmermann
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ...Pierre-Marie Pédrot
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the inner...Hugo Herbelin
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
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
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
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 #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record...coqbot-app[bot]
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" document...coqbot-app[bot]
2020-10-19Addressing parsing part #13078.Hugo Herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
2020-10-15Report a useful error for dependent destructionTej Chajed
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 03:49:55 +0000