aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2021-01-28Update doc/sphinx/proofs/writing-proofs/rewriting.rstJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2021-01-28Apply suggestions from code reviewThéo Zimmermann
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-28Document how rewrite works regarding occurrence selection.Théo Zimmermann
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
2021-01-22Merge PR #13754: Improve doc of occurrences and rewrite.coqbot-app[bot]
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
2021-01-22Improve doc of occurrences and rewrite.Jim Fehrle
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-21Merge PR #13764: Remove Add InjTyp and 10 other micromega commands (deprecate...BESSON Frederic
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Fix: "tactic" is not a tactic, so can't begin a .. tacn::Jim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2021-01-06Merge PR #13714: Changelog for 8.13.0coqbot-app[bot]
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
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-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
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-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-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-10Changelog for 8.12.2.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:00:03 +0000