coq/doc/sphinx/language, branch master The formal proof system Merge PR #14041: Enable canonical fun _ => _ projections. 2021-04-23T14:48:49+00:00 coqbot-app[bot] 2021-04-23T14:48:49+00:00 d332bbc3c1118631eb8c935ba61a8d071a90428e Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer 
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Extend Canonical Structure documentation. 2021-04-22T07:16:22+00:00 Jan-Oliver Kaiser 2020-05-15T09:44:29+00:00 9b35db9c7eb0cbc8e27c67f2ba2783fdd28ba247 This commit adds a more detailed explanation of what kinds of terms are allowed in fields of a canonical instance, how the fields are used as keys for canonical extension, what terms are considered overlapping, and how Coq reacts to overlapping fields. 
This commit adds a more detailed explanation of what kinds of terms are
allowed in fields of a canonical instance, how the fields are used as
keys for canonical extension, what terms are considered overlapping, and
how Coq reacts to overlapping fields.
Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
Merge PR #13815: Improve description of conversions 2021-04-19T09:14:24+00:00 coqbot-app[bot] 2021-04-19T09:14:24+00:00 8a49832ac5a4a9fab564c49ccef7146310db5bab Reviewed-by: Zimmi48 Ack-by: JasonGross 
Reviewed-by: Zimmi48
Ack-by: JasonGross
Improve conversion chapter. 2021-04-17T17:42:40+00:00 Jim Fehrle 2021-04-17T11:12:28+00:00 3e006e40fb213943e3e6574174a360ef866b0431 






Fix link in doc/cic.rst, there is no Credits chapter anymore
2021-04-10T17:31:49+00:00

Yannick Forster

2021-04-08T09:36:46+00:00

b3999ead5497a406653d1ae7c8c7af558d4c6595












Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












Convert 2nd part of rewriting chapter to prodn
2021-03-08T19:48:20+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

0d33024ff79c38d52fde49e23d0e45d9c22eefbe












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.







Properly document the local and global locality attributes.
2021-02-08T15:14:24+00:00

Théo Zimmermann

2021-02-06T17:39:25+00:00

4b08c87c99a72dd57bdd5b0be1bddd4085b4d495