aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
This makes it show the shape of the induction hypothesis in the second goal instead of just saying "subgoal 2 is S n <= S n".
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-23Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: gares
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
2020-04-23[documentation] ssreflect: Abbreviations do not support scopeKenji Maillard
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-23Fix coq snippets in Tactics chapter.Théo Zimmermann
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command ↵Pierre-Marie Pédrot
line -sprop-cumulative Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-04-22Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.Hugo Herbelin
2020-04-22Document Cauchy realsVincent Semeria
2020-04-22Document `+` in polymorphic universe levelsKenji Maillard
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 08:51:26 +0000