aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
2018-11-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
2018-11-23Doc for Private Polymorphic Universes.Gaëtan Gilbert
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-19Minor update to micromega.rstsoraros
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-09-25Remove romegaVincent Laporte
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Fix a few syntax highlighting issuesClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Remove an empty '.. bibliography::' in addendum/programClément Pit-Claudel
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Merge PR #8104: Warnings on coercions used without being ImportedEnrico Tassi
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Recover lost snippetMatěj G
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
2018-08-02Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ma...Théo Zimmermann
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', 'Om...Théo Zimmermann
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter 'Genera...Zeimer
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the R...Zeimer
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Microm...Zeimer
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', 'Prog...Théo Zimmermann
2018-07-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring a...Zeimer
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-13doc: fix typo.whitequark
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-09[sphinx] Improvements around the Show commands, including missing indices and...Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:32:27 +0000