aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-04-21Move documentation on Funind into a single file.Théo Zimmermann
2020-04-21Merge all documentation on Funind into the same file.Théo Zimmermann
2020-04-21Consolidate funind tactics and Functional Scheme in Funind section of the ↵Théo Zimmermann
Libraries chapter.
2020-04-21Extract funind tactics to funind section of the Libraries chapter.Théo Zimmermann
2020-04-21Remove parts of the Tactics chapter.Théo Zimmermann
2020-04-21Remove parts of the Tactics chapter.Théo Zimmermann
2020-04-21Remove everything in the Tactics chapter up-to function induction and a bit ↵Théo Zimmermann
beyond.
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
Omega was defined twice and this is the tactics chapter documentation which was refered to from the tactic index. We remove it so that users find the other reference (which contains the deprecation notice). The changes to the doc of zarith are a follow-up to #11976.
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
2020-04-20Remove funind tactics from Tactics chapter.Théo Zimmermann
2020-04-20Remove Functional Scheme from Scheme chapter.Théo Zimmermann
2020-04-20Move Functional Scheme to Funind section.Théo Zimmermann
2020-04-20Extract Functional Scheme from Scheme chapter.Théo Zimmermann
2020-04-20Remove probably useless doc/sphinx/coqdoc.css.Théo Zimmermann
2020-04-19CoqIDE: Adding a short documentation on style/theme customization.Hugo Herbelin
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
User time is unreliable for `native_compute`. Also output time spent in conversion to native code, just in case that is ever slow. Note that this also removes spurious newlines in the output. Fixes #11962
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-13Remove documentation for Hide menu in CoqIDE (was removed in 8.5).Théo Zimmermann
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-13doc for partial importsGaëtan Gilbert
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-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
We deprecate `Hide Obligations` and remove `Shrink Obligations` [deprecated since 8.7]
2020-04-09Merge PR #11534: Support universe bindings and universe constraints in Let ↵Gaëtan Gilbert
definitions. Reviewed-by: SkySkimmer
2020-04-08Merge PR #12005: Remove deprecated coqtop optionsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: ejgallego
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-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
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-02Document -rfrom option in reference manual.Théo Zimmermann
So far it was only documented in coqtop --help.
2020-04-02Remove deprecated -require option.Théo Zimmermann
This option is confusing because it does Require Import, not Require. It was deprecated in 8.11. We remove it in 8.12 in order to reintroduce it in 8.13 as a replacement for -load-vernac-object, which is the option that does Require without Import as of today.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 07:39:48 +0000