aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-21Merge PR #11311: Fix handling of recursive notations with custom entriesHugo Herbelin
2019-12-20Merge PR #11308: Fix complexity test-suite failure reporting on WinEnrico Tassi
2019-12-20Add test cases for #9490 and #9532Maxime Dénès
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-19Remove trailing \r in complexity measures for WindowsJason Gross
2019-12-19Better error reporting when res is not what is expectedJason Gross
2019-12-19Fix complexity test-suite failure reporting on WinJason Gross
2019-12-19Revert "Fix #11303: skip complexity tests on windows even if bogomips found"Jason Gross
2019-12-19Fix #11303: skip complexity tests on windows even if bogomips foundGaëtan Gilbert
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on only-p...Emilio Jesus Gallego Arias
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...Pierre-Marie Pédrot
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Merge PR #11198: Display more information when complexity tests failHugo Herbelin
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28Relax the pattern complexity testJason Gross
2019-11-27Display more information when complexity tests failJason Gross
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ...Pierre-Marie Pédrot
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
2019-11-26Update test-suite/complexity/pattern.vJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-25Add a complexity test for `pattern`Jason Gross
2019-11-22Add test for #11161Gaëtan Gilbert
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:24:03 +0000