aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-04-11Fix #7812Attila Gáspár
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10coqdoc: Report location of mismatched '[['Lysxia
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
to reflect lexer requirement for no space
2020-04-10Ignore subscripts in notation for matching cmds and tacsJim Fehrle
2020-04-10Fix prefix matchingJim Fehrle
2020-04-10Merge PR #11882: Adding a short form of Ltac2 Fresh.freshPierre-Marie Pédrot
Reviewed-by: MSoegtropIMC Reviewed-by: ppedrot Ack-by: tchajed
2020-04-10Change log for #12068 (Coqide segfault tentative fix).Hugo Herbelin
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 #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
Reviewed-by: anton-trunov
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-06Merge PR #12006: [coq_makefile] remove .lia.cache and .nia.cache by make ↵Enrico Tassi
cleanall Reviewed-by: gares
2020-04-05Adding package amssymb to support \lessgtr (apartness) in LaTeX output of ↵Hugo Herbelin
coqdoc.
2020-04-03Adding change log.Hugo Herbelin
2020-04-03Merge PR #11895: Remove Chapter command.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
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-03Update doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rstThéo Zimmermann
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-04-03Merge PR #11996: [stdlib] Add changelog for PR #11249Anton Trunov
Reviewed-by: anton-trunov
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-02Add changelog entry for #12005.Théo Zimmermann
2020-04-02remove .lia.cache and .nia.cache by make cleanallOlivier Laurent
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-02Remove Chapter command.Théo Zimmermann
This was an undocumented equivalent of the Section command.
2020-04-02Merge pull request #11993 from olaure01/ollibs-wfnat-changelogAnton Trunov
[stdlib] Add changelog for PR #11335
2020-04-01Merge PR #9803: Adding more trigonometry in RealsHugo Herbelin
Ack-by: MSoegtropIMC Ack-by: Zimmi48 Ack-by: herbelin
2020-04-01Merge pull request #11946 from olaure01/ollibs-permutationAnton Trunov
[stdlib] Add complementary results about Permutation
2020-04-01Add changelog for PR #11249Olivier Laurent
2020-04-01Merge PR #10592: coqdoc: Add a new `details' environment for coqdocLysxia
Reviewed-by: Lysxia Reviewed-by: Zimmi48
2020-04-01Add changelog for PR #11335Olivier Laurent
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-04-01- Addition to the Reals theory :thery
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties
2020-04-01Add complementary results about PermutationOlivier Laurent
2020-04-01add tests for notations with sigma typesOlivier Laurent
2020-04-01Merge PR #11960: Docgram use new no update optionEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-01Merge pull request #11880 from Lysxia/iterAnton Trunov
NArith, PArith: Add facts about iter
2020-03-31NArith, PArith: Add facts about iterLysxia
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 10:14:36 +0000