| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-30 | Remove the :> type cast | Jim Fehrle | |
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2021-01-25 | Remove the Hide Obligations flag | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-18 | Review commit: improving the doc of boolean attributes. | Théo Zimmermann | |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann | |
| The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. | |||
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle | |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-09-11 | [refman] Rename num to natural | Pierre Roux | |
| 2020-09-11 | Minimal changes to make the refman compatible with Sphinx 3. | Théo Zimmermann | |
| Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net> | |||
| 2020-05-13 | Merge PR #11828: [obligations] Deprecated flag cleanup | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 | |||
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-04-10 | [obligations] Deprecated flag cleanup | Emilio Jesus Gallego Arias | |
| We deprecate `Hide Obligations` and remove `Shrink Obligations` [deprecated since 8.7] | |||
| 2020-03-26 | Shrink refman-prelude files. | Théo Zimmermann | |
| 2020-03-19 | Document all the existing attributes. | Théo Zimmermann | |
| And fix documentation following the removal of the Template Check flag in #11546. | |||
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-11-01 | Update the deprecation doc of `Shrink Obligations` | Jason Gross | |
| Now it uses `.. deprecated` like all the other deprecation notices in the manual. | |||
| 2019-05-22 | [refman] Add more missing @ signs | Clément Pit-Claudel | |
| 2019-05-16 | [refman] Introduce syntax for alternatives in notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 2019-04-16 | Update and fix documentation of Program Fixpoint with measure | Maxime Dénès | |
| 2018-12-04 | Add undocumented options from mattam82 | Jim Fehrle | |
| 2018-12-03 | A few fixes of unexisting tokens. | Théo Zimmermann | |
| 2018-11-30 | Add indexes for coercion / substructure symbol :>. | Théo Zimmermann | |
| And a few more Sphinx fixes in passing. | |||
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 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] 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-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-01 | Merge PR #8192: Fix typos and typesetting of doc on Program | Théo Zimmermann | |
| 2018-07-30 | Fix typos and typesetting of doc on Program | Lysxia | |
| 2018-07-29 | Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵ | Zeimer | |
| and field' chapters of the Reference Manual. | |||
| 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-04-16 | [Sphinx] Clean-up indices | 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-03-29 | [Sphinx] Add chapter 24 | Maxime Dénès | |
| Thanks to Matthieu Sozeau for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 24 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |