aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/10-standard-library
AgeCommit message (Collapse)Author
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
add polynomial specifications of to_nat add changelog and doc entries
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-01-29add changelogOlivier Laurent
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
The original (which holds only for positive numbers) is now called exp_ineq1_pos. A version that holds only for negative numbers is added as exp_ineq1_neg. Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
2020-12-03Ascii: add leb and ltbYishuai Li
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
Reviewed-by: anton-trunov Reviewed-by: Blaisorblade
2020-11-13Add changelog for #13365Li-yao Xia
2020-11-04[stdlib] Decidable instance for negationYishuai Li
Added Changelog
2020-09-07Add changelog entryEdward Wang
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
Reviewed-by: erikmd Reviewed-by: herbelin
2020-08-12Additional statements about List.repeatOlivier Laurent
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2020-08-11add deprecation to changelogYishuai Li
2020-08-09Bring Int63 notations into line with stdlibJason Gross
We also put them in a module, so users can `Require Int63. Import Int63.Int63Notations` without needing to unqualify the primitives. In particular, we change - `a \% m` into `a mod m` to correspond with the notation in ZArith - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere - `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation The old notations are still accessible as deprecated notations. Fixes #12454
2020-08-09Bring Float notations in line with stdlibJason Gross
This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-05-12fuse changelogs for #11249 and #12237Olivier Laurent
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
Reviewed-by: pi8027 Reviewed-by: zeldovich
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-04add order properties about boolOlivier Laurent
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-05-02Adding change logs for PR #12121.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Also including feedback from Enrico Tassi.
2020-04-30do not re-export ListNotations from Program: changelogAntonio Nikishaev
2020-04-24[nsatz] Use Export rather than IncludeJason Gross
As per https://github.com/coq/coq/pull/12073#issuecomment-612869336
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 06:05:44 +0000