aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
2018-12-03[sphinx] Same rendering for :n:`@token` and :token:`token`.Théo Zimmermann
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-30Merge PR #9105: Add indexes for coercion / substructure symbol :>.Clément Pit-Claudel
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-28Fix numeral notations doc by indentingJason Gross
2018-11-28Fix string notation docJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
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-11-19Typo: comment does not match codeOlivier Laurent
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Print Universes SubgraphGaëtan Gilbert
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-06Improve rendering of the credits.Guillaume Melquiond
2018-11-01Merge PR #8845: Fix typos in the document about CICThéo Zimmermann
2018-10-30Credits for 8.9Matthieu Sozeau
2018-10-29Fix typos in the document about CICwkwkes
2018-10-24Merge PR #8813: Fix a few rendering issues in the manualThéo Zimmermann
2018-10-24Merge PR #8776: Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"Théo Zimmermann
2018-10-24[Manual] Prevent an irrelevant warning to show upVincent Laporte
2018-10-24[Manual] Avoid using deprecated “Focus”Vincent Laporte
2018-10-24[Manual] Fix rendering of an exampleVincent Laporte
2018-10-24[Manual] TypoVincent Laporte
2018-10-24[Manual] Fix an exampleVincent Laporte
2018-10-24[Manual] Fix layout of a listVincent Laporte
2018-10-23Merge PR #8798: Order Greek letters consistently w/rest of documentThéo Zimmermann
2018-10-23Fix formatting. Use standard if..then grammar.Sam Pablo Kuper
2018-10-23Order Greek letters consistently w/rest of documentSam Pablo Kuper
2018-10-19Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"Sam Pablo Kuper
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-13Merge PR #8616: Include the full Table of Contents document in the on-screen ...Clément Pit-Claudel
2018-10-13Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode.Clément Pit-Claudel
2018-10-11Documenting -arg in _CoqProject.Hugo Herbelin
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-10Merge PR #8384: Small fixes in attribute documentation.Clément Pit-Claudel
2018-10-10[doc] [sphinx] Fix title levels.Théo Zimmermann
2018-10-10Include all menu entries in the menu/short TOC so that users can viewJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 09:13:24 +0000