aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
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-04-03Move section on funind in appropriate location (inside libraries).Théo Zimmermann
2020-04-03Move section on implicit arguments in appropriate location (inside extensions).Théo Zimmermann
2020-04-03Extract section on implicit arguments from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on funind from Gallina extensions.Théo Zimmermann
2020-04-03Remove sections on records, sections, funind and implicit arguments from ↵Théo Zimmermann
gallina-ext chapter.
2020-04-03Extract section on sections from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on records from Gallina extensions.Théo Zimmermann
2020-04-03Adding changelog for 8.11.1.Pierre-Marie Pédrot
2020-04-02Merge PR #11869: Add an index for attributes.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-04-01Merge PR #10592: coqdoc: Add a new `details' environment for coqdocLysxia
Reviewed-by: Lysxia Reviewed-by: Zimmi48
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-28coqdoc: Add (* begin details *) and (* end details *)Thomas Letan
We propose to add an environment to have foldable texts with HTML output, more precisely: (*begin details [: An optional summary] *) some Coq and documentation material (* end details *) Currently, only the HTML output is supported. We could treat this environment in LaTeX output as appendixes to output later.
2020-03-27Split coqdoc section out of utility chapter (octopus merge).Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of both parts.
2020-03-27Move section on coqdoc to new location.Théo Zimmermann
2020-03-27Remove the part about coqdoc from the utilities chapter.Théo Zimmermann
(It was moved out onto a separate page.)
2020-03-27Prepare split of section about coqdoc.Théo Zimmermann
2020-03-26Merge PR #11929: Reintroduce a command that was actually used in another ↵Clément Pit-Claudel
one. Fix build of PDF manual. Reviewed-by: cpitclaudel
2020-03-26Reintroduce commands that were actually used. Fix build of PDF manual.Théo Zimmermann
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26CIC is printed in all-caps.Théo Zimmermann
As CIC is really an acronym, it should be printed in all-caps.
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of ↵Théo Zimmermann
coq_config Reviewed-by: Zimmi48
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line. The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed, then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
2020-03-20Add an index for attributes.Théo Zimmermann
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ↵Théo Zimmermann
fixed bug Reviewed-by: Zimmi48
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
Unfortunately, we cannot go further and parse Export as a legacy attribute because this syntax conflicts with the Export command.
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
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>
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 00:52:56 +0000