aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core
AgeCommit message (Collapse)Author
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18Run 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-16Update grammar in docJim Fehrle
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-14Move destructuring let syntax closer to its documentation.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-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-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-24Convert misc chapters to prodnJim Fehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-02More details in the documentation of native arraysVincent Semeria
Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Add persistent data structure Update doc/sphinx/language/core/primitive.rst Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-11[numeral notation] Improve documentationPierre Roux
Following reviews from Jim Fehrle on #12218 and #12979
2020-09-11[refman] Explicit integer and naturalPierre Roux
As respectively bigint and bignat that fit into an OCaml int.
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-18Use the new gdef alt-text feature in the refman.Théo Zimmermann
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Split Gallina into multiple files.Théo Zimmermann
2020-05-14Split parts of CIC into multiple files.Théo Zimmermann
2020-05-14Create new file on Functions and Assumptions.Théo Zimmermann
2020-05-14Merge definitions and type casts in same file.Théo Zimmermann
2020-05-14Create new file on Definitions.Théo Zimmermann
2020-05-14Add type casts to new Definitions file.Théo Zimmermann
2020-05-13Merge doc of modules from two origins.Théo Zimmermann
2020-05-13Move file on modules in new location.Théo Zimmermann
2020-05-13Add to file on modules.Théo Zimmermann
2020-05-13New file on primitive objects.Théo Zimmermann
2020-05-13Create a new file on conversion.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-12 12:20:42 +0000