aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/language
Commit message (Expand)AuthorAge
* Documenting the deprecation.Gravatar Pierre-Marie Pédrot2018-06-04
* Improve the last section of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
* Chapter 1 of the refman compiles without reporting any undocumented object.Gravatar Théo Zimmermann2018-05-28
* Improve sections on (Co)Fixpoint of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
* Improve subsection on co-inductive types of the Gallina chapter.Gravatar Théo Zimmermann2018-05-27
* Improve subsection on mutual inductive types of the Gallina chapter.Gravatar Théo Zimmermann2018-05-27
* Move 'new in Coq 8.1' subsection to an appropriate place.Gravatar Théo Zimmermann2018-05-27
* Document Variant properly.Gravatar Théo Zimmermann2018-05-27
* Improve inductive types subsection of the Gallina chapter.Gravatar Théo Zimmermann2018-05-27
* Improve subsection Definitions of the Gallina chapter.Gravatar Théo Zimmermann2018-05-26
* Improve subsection Assumptions of the Gallina chapter.Gravatar Théo Zimmermann2018-05-26
* Improve the section Terms of the Gallina chapter.Gravatar Théo Zimmermann2018-05-26
* [doc] Allow more than one signature and name per Sphinx objectGravatar Clément Pit-Claudel2018-05-25
* Document the new nested-proof error message.Gravatar Théo Zimmermann2018-05-21
* Document nested proofs and associated option.Gravatar Théo Zimmermann2018-05-17
* [doc] Address feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
* Remove duplicate entries for Proof, Qed, Defined, Admitted.Gravatar Théo Zimmermann2018-05-14
* [sphinx] Fix new warnings related to tacn, cmd, opt...Gravatar Théo Zimmermann2018-05-09
* [sphinx] Backport changes from #5979.Gravatar Théo Zimmermann2018-05-05
* Clean-up around cmd documentation.Gravatar Théo Zimmermann2018-05-05
* Fix error messages and make them consistent.Gravatar Théo Zimmermann2018-05-05
* Clean-up around options.Gravatar Théo Zimmermann2018-05-05
* [sphinx] Fix some references.Gravatar Théo Zimmermann2018-05-05
* Merge PR #7331: Fix a typo in the reference manual: <; -> <:Gravatar Maxime Dénès2018-04-26
|\
* \ Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bitGravatar Maxime Dénès2018-04-26
|\ \
| | * Fix a typo in the reference manual: <; -> <:Gravatar Kazuhiko Sakaguchi2018-04-23
| |/ |/|
* | [Sphinx] Clean-up indicesGravatar Maxime Dénès2018-04-16
* | [Sphinx] Fix a lot of references and description of optionsGravatar Maxime Dénès2018-04-16
* | [Sphinx] Fix all remaining warnings.Gravatar Maxime Dénès2018-04-14
* | [sphinx] Fix many warnings.Gravatar Théo Zimmermann2018-04-14
* | [Sphinx] Add Chapter 1Gravatar Maxime Dénès2018-04-13
* | [Sphinx] Move chapter 1 to new infrastructureGravatar Maxime Dénès2018-04-13
* | Merge PR #7222: [sphinx] Remove migration artefacts.Gravatar Maxime Dénès2018-04-12
|\ \
| * | [sphinx] Remove migration artefacts.Gravatar Théo Zimmermann2018-04-11
* | | [sphinx] Use macros for notes and examples.Gravatar Théo Zimmermann2018-04-11
* | | [sphinx] Fixes in chapter 2.Gravatar Théo Zimmermann2018-04-11
|/ /
| * Sphinx docs: clarify strict implicit argumentsGravatar Anton Trunov2018-04-05
|/
* [Sphinx] Remove duplicate entry for command `Coercion`Gravatar Maxime Dénès2018-03-29
* [doc] Port Chapter 20 Type Classes to SphinxGravatar Matthieu Sozeau2018-03-26
* [Sphinx] Add chapter 3Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 3 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Add chapter 5Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 5 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Add chapter 4Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 4 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Add chapter 2Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 2 to new infrastructureGravatar Maxime Dénès2018-03-15