aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-23Merge PR #13978: Do not match on record types with mutable fields in function...coqbot-app[bot]
2021-03-23Merge PR #13974: [cbn internal] env is a regular positional argumentPierre-Marie Pédrot
2021-03-23Do not match on record types with mutable fields in function arguments.Guillaume Melquiond
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
2021-03-22Merge PR #13225: Remove useless libobject for Implicit TypePierre-Marie Pédrot
2021-03-22[cbn internal] env is a regular positional argumentGaëtan Gilbert
2021-03-22Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic.coqbot-app[bot]
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
2021-03-19Remove useless libobject for Implicit TypeGaëtan Gilbert
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transit...Pierre-Marie Pédrot
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
2021-03-18Remove useless prefix argument in native compilation.Pierre-Marie Pédrot
2021-03-17Merge PR #13929: [ci] [gitlab] Remove ad-hoc mathcomp install macroscoqbot-app[bot]
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
2021-03-16Merge PR #13920: Adding an Ltac2 API to manipulate inductive types.coqbot-app[bot]
2021-03-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-03-16add results on to_listOlivier Laurent
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-16Adding an Ltac2 API to manipulate inductive types.Pierre-Marie Pédrot
2021-03-14Merge PR #13935: Fixed grammar productions for PDF documentationscoqbot-app[bot]
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
2021-03-13Merge PR #13917: Add deriving lib to CI.coqbot-app[bot]
2021-03-13Merge PR #13931: noglob/dumpglob should be in coqc specific usagecoqbot-app[bot]
2021-03-12Use the new API to prevent retyping of Ltac2 variable quotations.Pierre-Marie Pédrot
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
2021-03-12Merge PR #13907: Algorithmically faster algorithm for term replacing.coqbot-app[bot]
2021-03-12Further simplification of the term replacing code.Pierre-Marie Pédrot
2021-03-12Algorithmically faster algorithm for term replacing.Pierre-Marie Pédrot
2021-03-12Fixed grammar productions for PDF documentationsIsaac Oscar Gariano
2021-03-11Add deriving lib to CI.Arthur Azevedo de Amorim
2021-03-11noglob/dumpglob should be in coqc specific usageGaëtan Gilbert
2021-03-11Merge PR #13854: Normalize evars during bytecode compilation.coqbot-app[bot]
2021-03-10Fix kernel incorrectly assuming the "using" hyps are transitively closedGaëtan Gilbert
2021-03-10Merge PR #13922: Mention overlays in PR templatecoqbot-app[bot]
2021-03-10Mention overlays in PR templateGaëtan Gilbert
2021-03-10Merge PR #13901: Fix list contributorscoqbot-app[bot]
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-10Adding documentation of the changes.Pierre-Marie Pédrot
2021-03-10Adding a parsing test.Pierre-Marie Pédrot
2021-03-10Allow the presence of type casts for return values in Ltac2.Pierre-Marie Pédrot
2021-03-10Merge PR #13912: Refactor coercionopscoqbot-app[bot]
2021-03-10Merge PR #13919: Fix a hyperlink in CONTRIBUTING.mdcoqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-07 12:06:21 +0000