aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core
AgeCommit message (Collapse)Author
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
2020-05-13Merge sections on CoInductive types and co-recursive functions in new file.Théo Zimmermann
2020-05-13Add cofix and CoFixpoint to file on CoInductive types.Théo Zimmermann
2020-05-13Create new file on CoInductive types.Théo Zimmermann
2020-05-13Merge section on Inductive types from Gallina and CIC.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Merge sections on Inductive types and Recursive functions in new file.Théo Zimmermann
2020-05-13Add Recursive functions to new file on Inductive types.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Merge sections on variants and match into new file.Théo Zimmermann
2020-05-13Merge sections on Variants and Private inductive types into new file.Théo Zimmermann
2020-05-13Add match to new file on Variants.Théo Zimmermann
2020-05-13Create a new file on Variants.Théo Zimmermann
2020-05-13Create a new file on Variants.Théo Zimmermann
2020-05-13Create new file on sorts.Théo Zimmermann
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-06Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.Hugo Herbelin
2020-05-06Documenting 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-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 05:24:53 +0000