aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-03Support when release branch is checked out in a worktree.Théo Zimmermann
2020-04-03Add a rudimentary script to generate release changelog.Théo Zimmermann
The idea is very simple: use the list in the release branch to know which changelog entries to include, but do the work of removing these entries and consolidating the released changelog in the master branch (so that it is applied both to the master branch and to the release branch following the backporting process).
2020-04-03Merge PR #12009: Adding changelog for 8.11.1.Théo Zimmermann
Reviewed-by: Zimmi48
2020-04-03Fix CoRN CI script.Théo Zimmermann
Auto-generated files like the Makefile have recently been removed from the sources (cf. coq-community/corn#88). Calling ./configure.sh is now required.
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-02Minimal fix to man pages.Théo Zimmermann
2020-04-02Fix options listed in asycTaskQueue.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-02chore: Add missing [Register] for inductive types in Datatypes.vThomas Letan
We try to consistently register inductive types defined in the [Coq.Init.Datatypes] module, so that they can be fetch using [Coqlib.ref_lib]. We follow a naming scheme consistent with the rest of the module, that is: `core.<type name>.type' for the type, and `core.<type name>.<constructor name>' for the constructors.
2020-04-02Merge PR #12002: Cleanup tactic_option a bitPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-02Remove Chapter command.Théo Zimmermann
This was an undocumented equivalent of the Section command.
2020-04-02Cleanup tactic_option a bitGaëtan Gilbert
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-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-01Merge PR #11873: python3 script does not need to import from the futureEmilio Jesus Gallego Arias
Reviewed-by: JasonGross
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-04-01Merge PR #11960: Docgram use new no update optionEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-01Merge PR #11971: [ci] Run bignums' testsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-01Merge pull request #11880 from Lysxia/iterAnton Trunov
NArith, PArith: Add facts about iter
2020-04-01[lib] Remove custom backtrace destroying finalizersEmilio Jesus Gallego Arias
in favor of the one in the OCaml standard library.
2020-03-31Merge PR #11933: Fix calling test suite makefile with a dune built coqEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ↵Hugo Herbelin
arguments Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin
2020-03-31NArith, PArith: Add facts about iterLysxia
2020-03-31Merge PR #11915: [proof] Split delayed and regular proof closing functionsPierre-Marie Pédrot
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot
2020-03-31Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/Enrico Tassi
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaë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-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-31Merge PR #11823: [funind] [cleanup] Remove unused function parametersPierre-Marie Pédrot
Reviewed-by: Matafou Reviewed-by: ppedrot
2020-03-31[nit] [plugin_tuto] Remove empty function and use new API directlyEmilio Jesus Gallego Arias
2020-03-31[declare] [rewrite] Use high-level declare API, part II.Emilio Jesus Gallego Arias
2020-03-31[declare] [rewrite] Use high-level declare API, part I.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 18:33:10 +0000