coq/doc/stdlib, branch master The formal proof system Merge PR #14008: [stdlib] [Arith] Cantor pairing 2021-04-07T06:42:16+00:00 coqbot-app[bot] 2021-04-07T06:42:16+00:00 ae4c38571697528b96dd1f5319873dfe5a11d581 Reviewed-by: olaure01 Ack-by: jfehrle 
Reviewed-by: olaure01
Ack-by: jfehrle
Remove the omega tactic and related options 2021-04-03T01:52:59+00:00 Jim Fehrle 2021-01-11T22:47:13+00:00 d3a51ac24244f586dfeff1a93b68cb084370534e 






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







[build] Split stdlib to it's own opam package.
2021-03-03T15:06:14+00:00

Emilio Jesus Gallego Arias

2020-06-22T15:52:18+00:00

ab98d847d237af3cd0e46edef42218be65cfc98f

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.





We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.







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