| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-02-08 | Properly document the local and global locality attributes. | Théo Zimmermann | |
| 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-18 | Run doc_grammar for #13312. | 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-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-30 | Renaming Numeral.v into Number.v | Pierre Roux | |
| 2020-10-25 | Merge PR #12936: Convert misc chapters to prodn, update syntax | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: mattam82 Ack-by: pi8027 Ack-by: herbelin Ack-by: gares Ack-by: fajb Ack-by: proux01 | |||
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle | |
| 2020-10-23 | Correct doc using :>> | Gaëtan Gilbert | |
| The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106 | |||
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-09-11 | [numeral notation] Improve documentation | Pierre Roux | |
| Following reviews from Jim Fehrle on #12218 and #12979 | |||
| 2020-09-11 | [refman] Explicit integer and natural | Pierre Roux | |
| As respectively bigint and bignat that fit into an OCaml int. | |||
| 2020-09-11 | [refman] Rename int to integer | Pierre Roux | |
| 2020-09-11 | [refman] Rename numeral to number | Pierre Roux | |
| 2020-09-11 | [refman] Rename num to natural | Pierre Roux | |
| 2020-08-25 | Convert ltac2 chapter to use prodn, update syntax | Jim Fehrle | |
| 2020-06-09 | Minor improvements to the section on basics. | Théo Zimmermann | |
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle | |
| 2020-05-27 | Changelog entries for the 8.12 changes to the reference manual. | Théo Zimmermann | |
| 2020-05-18 | Use the new gdef alt-text feature in the refman. | Théo Zimmermann | |
| 2020-05-15 | Merge PR #11948: Hexadecimal numerals | Hugo Herbelin | |
| Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin | |||
| 2020-05-09 | [doc] Add hexadecimal numerals | Pierre Roux | |
| 2020-05-06 | Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann. | Hugo Herbelin | |
| 2020-05-06 | Documenting plugin/tactic/stdlib keywords in corresponding chapters. | Hugo Herbelin | |
| Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch || | |||
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-05-01 | Create basics out of sections from Gallina and Vernac chapters. | Théo Zimmermann | |
| 2020-05-01 | Create section on basics with just flags, options and tables. | Théo Zimmermann | |
| 2020-05-01 | Create section on basics with just lexical conventions and attributes. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |