coq/doc/changelog/10-standard-library, branch master The formal proof system add Cantor pairing to_nat and its inverse of_nat 2021-04-02T15:24:12+00:00 Andrej Dudenhefner 2021-03-25T17:19:12+00:00 2b02934f003836133d194d29f6a32c289280263c add polynomial specifications of to_nat add changelog and doc entries 
add polynomial specifications of to_nat
add changelog and doc entries
remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid 2021-03-26T08:15:49+00:00 Andrej Dudenhefner 2021-03-23T18:20:18+00:00 d7ccf45bbb1b73006c5804bcfc18bb3f6f7c90fd fix unexpectedly broken MSetGenTree.v add changelog entry 
fix unexpectedly broken MSetGenTree.v
add changelog entry
add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat 2021-03-23T08:21:42+00:00 Andrej Dudenhefner 2021-03-23T07:01:14+00:00 680ffd88630ac7f630533ce33d19200b8669f34a 






Merge PR #13671: [stdlib] [Vectors] add results on to_list
2021-03-23T08:01:22+00:00

coqbot-app[bot]

2021-03-23T08:01:22+00:00

1f7875b9c457aad27cd5ee8bfe2dd12898926cb2

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







Merge PR #13804: [stdlib] [List] Add results about count_occ
2021-03-23T08:00:38+00:00

coqbot-app[bot]

2021-03-23T08:00:38+00:00

7c9bb01b485cb3fd4b997125fbe2e4acb735054f

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







correct changelog #13582
2021-03-16T20:06:41+00:00

Olivier Laurent

2020-12-28T18:14:13+00:00

e38f64e024c94ad188e186506356980534ab604b












add changelog
2021-03-16T20:06:41+00:00

Olivier Laurent

2020-12-24T12:02:23+00:00

36a54c1d891c6d853a218e66f9ce8f011311c855












Signed primitive integers
2021-02-26T13:32:41+00:00

Ana

2020-12-01T08:52:12+00:00

4302a75d82b9ac983cd89dd01c742c36777d921b

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.





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.







Merge PR #13080: Ascii: add leb and ltb
2021-02-25T11:08:08+00:00

coqbot-app[bot]

2021-02-25T11:08:08+00:00

87fc1db11d152af38b5e0d01d7ba925035c396a9

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







add changelog
2021-01-29T21:25:46+00:00

Olivier Laurent

2021-01-29T07:53:20+00:00

5b9da3b6bdb4ee44b817313274f9d8fc87f66234