aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-03-31Merge PR #14035: Fix printing of ssr do intros and seq tacticscoqbot-app[bot]
2021-03-31Fix printing of ssr do intros and seq tacticsLasse Blaauwbroek
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to...coqbot-app[bot]
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-10Adding output tests.Pierre-Marie Pédrot
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-04[test-suite] test for primitive tokens in patternsEnrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-02-26Signed primitive integersAna
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-20Merge PR #13744: Make sure "Print Module" write a dot at the end of inductive...coqbot-app[bot]
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
2021-01-04Temporarily deactivating printing check for cases.Pierre-Marie Pédrot
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-09Constrintern: Code factorization in interning of record fields.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-12-08Congruence: don't replace error messages by "congruence failed"Gaëtan Gilbert
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Put all Int63 primitives in a separate filePierre Roux
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-25Clean UnivBinders testGaëtan Gilbert
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...coqbot-app[bot]
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:40:17 +0000