aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2021-01-06Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-m...coqbot-app[bot]
2021-01-06Merge PR #13714: Changelog for 8.13.0coqbot-app[bot]
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Changelog for 8.13.0Enrico Tassi
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
2020-12-14Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction P...Pierre-Marie Pédrot
2020-12-13Merge PR #13619: doc: Clarify the status of simpl vs cbncoqbot-app[bot]
2020-12-13Add changelog for #13509.Hugo Herbelin
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-11doc: Clarify the status of simpl vs cbnClément Pit-Claudel
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11Merge PR #13611: Clarify changelog categories.Clément Pit-Claudel
2020-12-11Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 re...Clément Pit-Claudel
2020-12-11Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds foral...coqbot-app[bot]
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-11Bump reference to 8.12 refman following unexpected 8.12.2 release.Théo Zimmermann
2020-12-11Clarify changelog categories.Théo Zimmermann
2020-12-10Changelog for 8.12.2.Théo Zimmermann
2020-12-09Merge PR #13564: Allow all characters in tacn, cmd, ... names. Report duplic...Clément Pit-Claudel
2020-12-09Allow any character in a tacn, cmd, ... nameJim Fehrle
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-05Merge PR #13553: Document Number Notation for primitive integerscoqbot-app[bot]
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-12-04Merge PR #13569: typocoqbot-app[bot]
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
2020-12-04typoYves Bertot
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-03Ascii: add leb and ltbYishuai Li
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:50:07 +0000