aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-27Merge PR #13167: Ltac2: use ComTactic infrastructurePierre-Marie Pédrot
2020-10-27Merge PR #13260: [CI cachix] Force-delete pr branches.coqbot-app[bot]
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-26Ltac2: use ComTactic infrastructureGaëtan Gilbert
2020-10-26Improve tactic interpreter registration API a bitGaëtan Gilbert
2020-10-26Yet another normal / neutral bug in primitive conversion.Pierre-Marie Pédrot
2020-10-26Fix bug in conversion of primitive values.Pierre-Marie Pédrot
2020-10-26Merge PR #13257: adjust Search deprecation warningcoqbot-app[bot]
2020-10-26Merge PR #13223: [declare] Remove recursive declaration from non-recursive fu...coqbot-app[bot]
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
2020-10-26adjust Search deprecation warningRalf Jung
2020-10-26Merge PR #13137: [ltac] Avoid magic numberscoqbot-app[bot]
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-24Merge PR #13263: Correct doc using :>>coqbot-app[bot]
2020-10-23Correct doc using :>>Gaëtan Gilbert
2020-10-23Merge PR #13261: Fix overlay merge commandcoqbot-app[bot]
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
2020-10-23Fix overlay merge commandGaëtan Gilbert
2020-10-23Force-delete pr branches.Théo Zimmermann
2020-10-23Merge PR #13177: Automatically merge overlays with most recent upstream versioncoqbot-app[bot]
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
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-22Make sure that setoid_rewrite passes state to subgoalsLasse Blaauwbroek
2020-10-22Micro-optimization in Control.check_for_interrupt.Pierre-Marie Pédrot
2020-10-22Merge PR #13243: Fix bench variablesPierre-Marie Pédrot
2020-10-22Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env.Vincent Laporte
2020-10-22[default.nix] Propagate OCaml and findlib to user env.Théo Zimmermann
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under l...Pierre-Marie Pédrot
2020-10-22Fix bench variablesGaëtan Gilbert
2020-10-22Merge PR #13198: [coqinit] Respect order of ML includescoqbot-app[bot]
2020-10-21[coqinit] Cosmetics on long list append.Emilio Jesus Gallego Arias
2020-10-21[coqinit] Respect order of ML includesEmilio Jesus Gallego Arias
2020-10-21Merge PR #13222: Bench: move variables to the scriptPierre-Marie Pédrot
2020-10-21Add overlays.Pierre-Marie Pédrot
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Document the signatures of quotient names in the API.Pierre-Marie Pédrot
2020-10-21Introduce the missing dual name quotient modules in Environ.Pierre-Marie Pédrot
2020-10-21Code factorization in Names.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 08:34:24 +0000