Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7920: Generic syntax for attributes | 2018-07-09 | |
|\ | |||
* | | doc: Fix markup in Calculus of Inductive Constructions | 2018-07-04 | |
| | | |||
| * | Describe attributes in the documentation. | 2018-07-03 | |
|/ | |||
* | Merge PR #7703: Add an option to force parameters to be uniform | 2018-07-02 | |
|\ | |||
* \ | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | 2018-07-02 | |
|\ \ | |||
| | * | Document option Uniform Inductive Parameters | 2018-07-01 | |
| | | | |||
| * | | doc: typesetting and hyperlinks in Syntax Extensions | 2018-06-30 | |
| |/ | |||
* / | doc: Fix typesetting in Gallina extensions | 2018-06-29 | |
|/ | |||
* | wrong sphinx syntax | 2018-06-28 | |
| | |||
* | Update gallina-extensions.rst | 2018-06-28 | |
| | | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual | ||
* | Documenting the syntax of mutual keywords. | 2018-06-24 | |
| | |||
* | [sphinx] Finish clean-up of the Canonical Structure subsection. | 2018-06-16 | |
| | |||
* | doc: Add "Print Canonical Projections" command to Command index | 2018-06-16 | |
| | |||
* | Documenting the deprecation. | 2018-06-04 | |
| | |||
* | Improve the last section of the Gallina chapter. | 2018-05-28 | |
| | |||
* | Chapter 1 of the refman compiles without reporting any undocumented object. | 2018-05-28 | |
| | |||
* | Improve sections on (Co)Fixpoint of the Gallina chapter. | 2018-05-28 | |
| | |||
* | Improve subsection on co-inductive types of the Gallina chapter. | 2018-05-27 | |
| | |||
* | Improve subsection on mutual inductive types of the Gallina chapter. | 2018-05-27 | |
| | |||
* | Move 'new in Coq 8.1' subsection to an appropriate place. | 2018-05-27 | |
| | |||
* | Document Variant properly. | 2018-05-27 | |
| | | | | | | Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121 This commit also marginally improves the Record doc (a lot more remains to do). | ||
* | Improve inductive types subsection of the Gallina chapter. | 2018-05-27 | |
| | |||
* | Improve subsection Definitions of the Gallina chapter. | 2018-05-26 | |
| | |||
* | Improve subsection Assumptions of the Gallina chapter. | 2018-05-26 | |
| | |||
* | Improve the section Terms of the Gallina chapter. | 2018-05-26 | |
| | | | | Including adding missing irrefutable-patterns to the grammar of binders. | ||
* | [doc] Allow more than one signature and name per Sphinx object | 2018-05-25 | |
| | | | | As discussed in GH-7556. | ||
* | Document the new nested-proof error message. | 2018-05-21 | |
| | |||
* | Document nested proofs and associated option. | 2018-05-17 | |
| | |||
* | [doc] Address feedback on doc writer guide | 2018-05-15 | |
| | | | | Co-Authored-By: @Zimmi48 | ||
* | Remove duplicate entries for Proof, Qed, Defined, Admitted. | 2018-05-14 | |
| | | | | And marginal improvements in the last section of the Gallina chapter. | ||
* | [sphinx] Fix new warnings related to tacn, cmd, opt... | 2018-05-09 | |
| | |||
* | [sphinx] Backport changes from #5979. | 2018-05-05 | |
| | |||
* | Clean-up around cmd documentation. | 2018-05-05 | |
| | | | | In particular, remove trailing dots. | ||
* | Fix error messages and make them consistent. | 2018-05-05 | |
| | | | | All the error messages start with a capitalized letter and end with a dot. | ||
* | Clean-up around options. | 2018-05-05 | |
| | | | | | | - Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`. | ||
* | [sphinx] Fix some references. | 2018-05-05 | |
| | |||
* | Merge PR #7331: Fix a typo in the reference manual: <; -> <: | 2018-04-26 | |
|\ | |||
* \ | Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bit | 2018-04-26 | |
|\ \ | |||
| | * | Fix a typo in the reference manual: <; -> <: | 2018-04-23 | |
| |/ |/| | |||
* | | [Sphinx] Clean-up indices | 2018-04-16 | |
| | | |||
* | | [Sphinx] Fix a lot of references and description of options | 2018-04-16 | |
| | | |||
* | | [Sphinx] Fix all remaining warnings. | 2018-04-14 | |
| | | |||
* | | [sphinx] Fix many warnings. | 2018-04-14 | |
| | | | | | | | | | | Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | ||
* | | [Sphinx] Add Chapter 1 | 2018-04-13 | |
| | | |||
* | | [Sphinx] Move chapter 1 to new infrastructure | 2018-04-13 | |
| | | |||
* | | Merge PR #7222: [sphinx] Remove migration artefacts. | 2018-04-12 | |
|\ \ | |||
| * | | [sphinx] Remove migration artefacts. | 2018-04-11 | |
| | | | | | | | | | | | | | | | These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target. | ||
* | | | [sphinx] Use macros for notes and examples. | 2018-04-11 | |
| | | | |||
* | | | [sphinx] Fixes in chapter 2. | 2018-04-11 | |
|/ / | | | | | | | Mostly using the good option macros. | ||
| * | Sphinx docs: clarify strict implicit arguments | 2018-04-05 | |
|/ |