aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
Co-authored-by: Jasper Hugunin <jasper@hugunin.net> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-31[nit] [plugin_tuto] Remove empty function and use new API directlyEmilio Jesus Gallego Arias
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
Ack-by: Matafou Reviewed-by: SkySkimmer
2020-03-31Merge PR #11131: [ci] [gitlab] Add test-suite test for OCaml 4.10 and 4.11Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`.
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
The only reasons that `prepare_definition` returned a sigma were: - to obtain the universe binders to be passed to declare - to obtain the UState.t to be passed to the equations hook We handle this automatically now; it seems like a reasonably good API improvement. However, it is not clear what we do now is right for all cases; must check.
2020-03-30[declare] [obligations] Refactor preparation of obligation entryEmilio Jesus Gallego Arias
Preparation of obligation/program entries requires low-level manipulation that does break the abstraction over `proof_entry`; we thus introduce `prepare_obligation`, and move the code that prepares the obligation entry to its own module. This seems to improve separation of concerns, and helps clarify the two of three current models in which Coq operates w.r.t. definitions: - single, ground entries with possibly mutual definitions [regular lemmas] - single, non-ground entries with possibly mutual definitions [obligations] - multiple entries [equations]
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-03-30[dune] [docgram] Remove bash hack thanks to new option -no-update.Théo Zimmermann
2020-03-30Merge PR #11958: Add -no-update command line option to doc_grammar for DuneThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
Ack-by: Zimmi48 Reviewed-by: anton-trunov Ack-by: jfehrle Reviewed-by: maximedenes
2020-03-29[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11Emilio Jesus Gallego Arias
2020-03-29Update 11909-fix-≡-level.rstJason Gross
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
Fix makefile glitches
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
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-28Update fullGrammar and orderedGrammar following #11877.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
Use `dune build @check-gram --auto-promote` to automatically update these two files. You will need to run it twice if the two files need to be updated (which is the case most often) as Dune will stop after the first diff failure. The rst files are also updated but left in the `_build/` directory as Dune wouldn't support targets outside the current directory. You can just `mv _build/default/doc/sphinx doc` to update them after running the @check-gram target.
2020-03-27Fix changelogVincent Semeria
2020-03-27Merge PR #11871: Split documentation of coqdoc on separate page.Clément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 14:22:38 +0000