| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle | |
| 2020-11-18 | [attributes] Update error message referring to deprecated syntax. | Emilio Jesus Gallego Arias | |
| 2020-11-18 | Review commit: improving the doc of boolean attributes. | Théo Zimmermann | |
| 2020-11-18 | [attributes] Deprecate `attr(true)` syntax in favor of booelan attributes. | Emilio Jesus Gallego Arias | |
| We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog. | |||
| 2020-11-16 | Doc for variance syntax | Gaëtan Gilbert | |
| 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-06-09 | Minor improvements to the section on sorts. | Théo Zimmermann | |
| 2020-05-14 | Reintroduce leftover parts; update index files; small fixes. | Théo Zimmermann | |
| 2020-04-22 | Document `+` in polymorphic universe levels | Kenji Maillard | |
| 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-03-09 | Remove some productionlists | Jim Fehrle | |
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2020-01-21 | Reference manual: Typos/English in chapter universe polymorphism. | Hugo Herbelin | |
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-10-02 | Loosen restrictions on mixing universe mono/polymorphism in sections | Gaëtan Gilbert | |
| We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel. | |||
| 2019-09-25 | Adding documentation for the move of sections data to kernel. | Pierre-Marie Pédrot | |
| 2019-07-18 | Adding changelog and documentation. | Pierre-Marie Pédrot | |
| 2019-05-23 | Define many undefined tokens, and other misc fixes. | Théo Zimmermann | |
| Progress towards #9411, extracted from #10118, rebased ontop of #10192. | |||
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-02-12 | Fix failing coqtops universe-polymorphism.rst | Gaëtan Gilbert | |
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-23 | Doc for Private Polymorphic Universes. | Gaëtan Gilbert | |
| 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-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 | Improved grammar and spelling in the remaining chapters of the Reference Manual. | Zeimer | |
| 2018-05-09 | [sphinx] Improvements around the Show commands, including missing indices ↵ | Théo Zimmermann | |
| and indentation. | |||
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | [sphinx] Use option direct reference. | Théo Zimmermann | |
| 2018-04-12 | [Sphinx] Add chapter 29 | Maxime Dénès | |
| Thanks to Clément Pit Claudel for porting this chapter. Backport universe polymorphism changes from 2017 and 2018. | |||
| 2018-04-11 | [Sphinx] Move chapter 29 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |