aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core
AgeCommit message (Collapse)Author
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
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
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-03Split four sections out of the Gallina extensions chapter.Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of all the parts.
2020-04-03Move section in records in appropriate location (inside core).Théo Zimmermann
2020-04-03Move section on sections in appropriate location (inside core).Théo Zimmermann
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 15:04:19 +0000