aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-02Merge PR #13250: Micro-optimization in Control.check_for_interrupt.coqbot-app[bot]
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
2020-11-02Merge PR #13294: Update screenshot of shield icon (shown in CONTRIBUTING).coqbot-app[bot]
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ...Pierre-Marie Pédrot
2020-11-02Merge PR #13145: Adding support for printing goal names in CoqIDEPierre-Marie Pédrot
2020-11-02Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" w...Pierre-Marie Pédrot
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-11-02Update screenshot of shield icon (shown in CONTRIBUTING).Théo Zimmermann
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02add changelogEnrico Tassi
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02document Proof.compactEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Add change log for #13145.Hugo Herbelin
2020-10-30Adding support for printing goal names in CoqIDE.Hugo Herbelin
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
2020-10-28Adding changelog for #13247.Hugo Herbelin
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the inner...Hugo Herbelin
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
2020-10-27Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg g...coqbot-app[bot]
2020-10-27Merge PR #13226: Restore the List.Smart.map original implementation.coqbot-app[bot]
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 00:45:15 +0000