aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-13Set the lsb of return addresses on the bytecode interpreter stack.Guillaume Melquiond
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-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
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-10Adding output tests.Pierre-Marie Pédrot
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Allow to register deprecation status in Ltac2 term and notation declarations.Pierre-Marie Pédrot
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]
2021-03-10Fix a hyperlink in CONTRIBUTING.mdKazuhiko Sakaguchi
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-09Add overlayKazuhiko Sakaguchi
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-07Merge PR #13910: Attempt to fix the bench after coq-core splitPierre-Marie Pédrot
2021-03-07Attempt to fix the bench after coq-core splitGaëtan Gilbert
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-06Inline the refold and tactic_mode flags for the cbn tactic.Pierre-Marie Pédrot
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-06Merge PR #13902: [coercion] expose coercion_infoPierre-Marie Pédrot
2021-03-06Merge PR #13899: Add noncritical constraint to exception catching in solve_co...Pierre-Marie Pédrot
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-05[coercipn] expose coercion_infoEnrico Tassi
2021-03-05Update nixpkgs.Théo Zimmermann
2021-03-05Fix the .mailmap.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:25:37 +0000