coq/doc/stdlib/index-list.html.template, 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
Adding a changelog and registering the new file in the documentation. 2021-03-16T19:02:56+00:00 Pierre-Marie Pédrot 2021-03-10T13:07:46+00:00 761d3ccaf6a593a73811da38fa731c2f601902f8 






Merge PR #13236: Add a type of format strings to Ltac2.
2021-03-06T16:25:33+00:00

Michael Soegtrop

2021-03-06T16:25:33+00:00

2c47f51a9b03b962cf688967f2ad1bdf0df448c9

Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC





Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC







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.







Add a type of format strings to Ltac2.
2021-01-22T10:55:21+00:00

Pierre-Marie Pédrot

2020-06-25T21:35:20+00:00

0c1af31e9d338a13b7df2b4468b81e76ef182d32

It provides an abstract type of well-typed format strings, a scope to parse
them and a minimal printf-like API.





It provides an abstract type of well-typed format strings, a scope to parse
them and a minimal printf-like API.







Merge PR #13275: Put all Int63 primitives in a separate file
2020-12-02T15:57:04+00:00

Vincent Laporte

2020-12-02T15:57:04+00:00

11730fa0ed2cb10da1ffc00f4f1140572134937e

Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl





Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl







Put all Int63 primitives in a separate file
2020-12-02T08:26:53+00:00

Pierre Roux

2020-10-26T13:43:05+00:00

853b838681db635f51fc3c7ba3dfe26bc6712d72

Following a request from Pierre-Marie Pédrot in #13258





Following a request from Pierre-Marie Pédrot in #13258







Update compat infrastructure for 8.14
2020-11-23T15:47:06+00:00

Enrico Tassi

2020-11-23T15:47:06+00:00

17da7c41b17da3280cb2c182387685ad4be6022f












[compat] remove 8.10
2020-11-09T13:55:23+00:00

Enrico Tassi

2020-11-09T13:55:23+00:00

a028e70817e7fd43b35643a8faa9bc7f59897ddb












[numeral notation] Specify R
2020-11-04T23:20:19+00:00

Pierre Roux

2020-09-03T11:20:00+00:00

edea770457aea05a7e6a64c1217f66dfc6930419