aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core/basic.rst
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-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
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 #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
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
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:04:49 +0000