| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-28 | wrong sphinx syntax | Ambroise | |
| 2018-06-28 | Update gallina-extensions.rst | Ambroise | |
| I knew this feature existed but I did not remember the syntax and I could not find it in the manual | |||
| 2018-06-24 | Documenting the syntax of mutual keywords. | Pierre-Marie Pédrot | |
| 2018-06-16 | [sphinx] Finish clean-up of the Canonical Structure subsection. | Théo Zimmermann | |
| 2018-06-16 | doc: Add "Print Canonical Projections" command to Command index | Anton Trunov | |
| 2018-06-04 | Documenting the deprecation. | Pierre-Marie Pédrot | |
| 2018-05-28 | Improve the last section of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-28 | Chapter 1 of the refman compiles without reporting any undocumented object. | Théo Zimmermann | |
| 2018-05-28 | Improve sections on (Co)Fixpoint of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-27 | Improve subsection on co-inductive types of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-27 | Improve subsection on mutual inductive types of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-27 | Move 'new in Coq 8.1' subsection to an appropriate place. | Théo Zimmermann | |
| 2018-05-27 | Document Variant properly. | Théo Zimmermann | |
| 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). | |||
| 2018-05-27 | Improve inductive types subsection of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-26 | Improve subsection Definitions of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-26 | Improve subsection Assumptions of the Gallina chapter. | Théo Zimmermann | |
| 2018-05-26 | Improve the section Terms of the Gallina chapter. | Théo Zimmermann | |
| Including adding missing irrefutable-patterns to the grammar of binders. | |||
| 2018-05-25 | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | |
| As discussed in GH-7556. | |||
| 2018-05-21 | Document the new nested-proof error message. | Théo Zimmermann | |
| 2018-05-17 | Document nested proofs and associated option. | Théo Zimmermann | |
| 2018-05-15 | [doc] Address feedback on doc writer guide | Clément Pit-Claudel | |
| Co-Authored-By: @Zimmi48 | |||
| 2018-05-14 | Remove duplicate entries for Proof, Qed, Defined, Admitted. | Théo Zimmermann | |
| And marginal improvements in the last section of the Gallina chapter. | |||
| 2018-05-09 | [sphinx] Fix new warnings related to tacn, cmd, opt... | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Backport changes from #5979. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Fix error messages and make them consistent. | Théo Zimmermann | |
| All the error messages start with a capitalized letter and end with a dot. | |||
| 2018-05-05 | Clean-up around options. | Théo Zimmermann | |
| - Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`. | |||
| 2018-05-05 | [sphinx] Fix some references. | Théo Zimmermann | |
| 2018-04-26 | Merge PR #7331: Fix a typo in the reference manual: <; -> <: | Maxime Dénès | |
| 2018-04-26 | Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bit | Maxime Dénès | |
| 2018-04-23 | Fix a typo in the reference manual: <; -> <: | Kazuhiko Sakaguchi | |
| 2018-04-16 | [Sphinx] Clean-up indices | Maxime Dénès | |
| 2018-04-16 | [Sphinx] Fix a lot of references and description of options | Maxime Dénès | |
| 2018-04-14 | [Sphinx] Fix all remaining warnings. | Maxime Dénès | |
| 2018-04-14 | [sphinx] Fix many warnings. | Théo Zimmermann | |
| Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | |||
| 2018-04-13 | [Sphinx] Add Chapter 1 | Maxime Dénès | |
| 2018-04-13 | [Sphinx] Move chapter 1 to new infrastructure | Maxime Dénès | |
| 2018-04-12 | Merge PR #7222: [sphinx] Remove migration artefacts. | Maxime Dénès | |
| 2018-04-11 | [sphinx] Remove migration artefacts. | Théo Zimmermann | |
| These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target. | |||
| 2018-04-11 | [sphinx] Use macros for notes and examples. | Théo Zimmermann | |
| 2018-04-11 | [sphinx] Fixes in chapter 2. | Théo Zimmermann | |
| Mostly using the good option macros. | |||
| 2018-04-05 | Sphinx docs: clarify strict implicit arguments | Anton Trunov | |
| 2018-03-29 | [Sphinx] Remove duplicate entry for command `Coercion` | Maxime Dénès | |
| 2018-03-26 | [doc] Port Chapter 20 Type Classes to Sphinx | Matthieu Sozeau | |
| 2018-03-15 | [Sphinx] Add chapter 3 | Maxime Dénès | |
| Thanks to Pierre Letouzey for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 3 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 5 | Maxime Dénès | |
| Thanks to Richard Ford for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 5 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 4 | Maxime Dénès | |
| Thanks to Richard Ford for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 4 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |