| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-25 | Remove romega | Vincent Laporte | |
| 2018-09-20 | Rewrite "Flags, Options and Tables" section. | Jim Fehrle | |
| Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: | |||
| 2018-09-20 | [doc] Fix a few syntax highlighting issues | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Remove an empty '.. bibliography::' in addendum/program | Clément Pit-Claudel | |
| 2018-09-11 | Merge PR #8425: Deprecate romega in favor of lia | Pierre-Marie Pédrot | |
| 2018-09-10 | Merge PR #8104: Warnings on coercions used without being Imported | Enrico Tassi | |
| 2018-09-10 | Deprecate romega in favor of lia. | Vincent Laporte | |
| 2018-09-07 | Recover lost snippet | Matěj G | |
| This snippet on pattern matching got lost in the process of migrating to Sphynx. | |||
| 2018-09-07 | Warnings on coercions used without being Imported | Maxime Dénès | |
| This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes. | |||
| 2018-08-31 | Fixed the seealso directive in a few places. | Zeimer | |
| 2018-08-31 | Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵ | Zeimer | |
| directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues. | |||
| 2018-08-03 | Fix docs on arguments to setoid_replace. Fixes #8213 | Langston Barrett | |
| 2018-08-02 | Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ↵ | Théo Zimmermann | |
| matching' of the Reference Manual. | |||
| 2018-08-02 | Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', ↵ | Théo Zimmermann | |
| 'Omega' and 'Micromega' of the Reference Manual. | |||
| 2018-08-01 | Added a tactic index entry for nsatz, reformatted commands in chapter ↵ | Zeimer | |
| 'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter. | |||
| 2018-08-01 | Improved grammar and spelling in the remaining chapters of the Reference Manual. | Zeimer | |
| 2018-08-01 | Improved grammar and spelling in chapter 'Extended pattern matching' of the ↵ | Zeimer | |
| Reference Manual. | |||
| 2018-08-01 | Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵ | Zeimer | |
| 'Micromega' of the Reference Manual. | |||
| 2018-08-01 | Merge PR #8192: Fix typos and typesetting of doc on Program | Théo Zimmermann | |
| 2018-08-01 | Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', ↵ | Théo Zimmermann | |
| 'Program' and 'ring and field' chapters of the Reference Manual. | |||
| 2018-07-30 | Fix typos and typesetting of doc on Program | Lysxia | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clément Pit-Claudel | |
| Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines. | |||
| 2018-07-29 | Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵ | Zeimer | |
| and field' chapters of the Reference Manual. | |||
| 2018-07-26 | Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵ | Zeimer | |
| Reference Manual. | |||
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-06-25 | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | |
| 2018-06-19 | [doc] Use productionlist instead of prodn in ring.rst | Clément Pit-Claudel | |
| 2018-06-13 | doc: fix typo. | whitequark | |
| 2018-06-08 | Existing Class noop when already a class + warning. | Gaëtan Gilbert | |
| Fix #5012. | |||
| 2018-05-16 | Typo in documentation of Derive | Joachim Breitner | |
| 2018-05-15 | [doc] Address feedback on doc writer guide | Clément Pit-Claudel | |
| Co-Authored-By: @Zimmi48 | |||
| 2018-05-15 | [doc] Small fixes | Clément Pit-Claudel | |
| 2018-05-14 | Merge PR #7374: [sphinx] More fatal warnings. | Maxime Dénès | |
| 2018-05-09 | [sphinx] Improvements around the Show commands, including missing indices ↵ | Théo Zimmermann | |
| and indentation. | |||
| 2018-05-09 | [sphinx] Fix new warnings related to tacn, cmd, opt... | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improve typeclass chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Re-indent to get much better rendering. | Théo Zimmermann | |
| Add some more cmd references. And use deprecated directives. | |||
| 2018-05-05 | Two more uses of verbatim in doc. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Add some refs in the Omega chapter. | Théo Zimmermann | |
| 2018-05-05 | More fixes in the Generalized Rewriting chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] More use of cmd references in Extraction chapter. | Théo Zimmermann | |
| 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 | Fix failing example in refman. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix some references. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use option direct reference. | Théo Zimmermann | |
| 2018-05-05 | Fix typo in Coercions chapter. | Théo Zimmermann | |
| 2018-04-16 | [Sphinx] Clean-up indices | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |