aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
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
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Move extended pattern matching to new location.Théo Zimmermann
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
2020-04-27Further documentation improvements.Théo Zimmermann
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-22Document `+` in polymorphic universe levelsKenji Maillard
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:31:12 +0000