aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-16[zify] bugfixFrederic Besson
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-30Remove the :> type castJim Fehrle
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-14Update zify documentationFrédéric Besson
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
2020-05-16Add redirects for HTML pages that were moved.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:51:21 +0000