coq/doc/sphinx/language/core, branch master The formal proof system 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
Improve conversion chapter. 2021-04-17T17:42:40+00:00 Jim Fehrle 2021-04-17T11:12:28+00:00 3e006e40fb213943e3e6574174a360ef866b0431 






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












Fix hierarchy of sections in module chapter.
2021-02-05T21:13:07+00:00

Théo Zimmermann

2021-02-05T21:13:07+00:00

9dae1a0c23cae4d655a40cefc5c59c3dcb8fdbf8












Replace : term with : type in open binders.
2021-01-28T20:22:44+00:00

Théo Zimmermann

2021-01-28T20:22:44+00:00

f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9

And update the doc_grammar files.





And update the doc_grammar files.







Convert rewriting and proof-mode chapters to prodn
2020-12-30T19:48:37+00:00

Jim Fehrle

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

e02120ed6580733db2276f0c11b4f432ea670ee3












[refman] Fix error names.
2020-12-03T10:33:31+00:00

Théo Zimmermann

2020-12-03T09:33:33+00:00

6a3586d80dd068c2067a8e47effed8122d0bd3b3

The @ syntax is not supported in the name, so we transform it manually
as it would have been if no name had been provided.





The @ syntax is not supported in the name, so we transform it manually
as it would have been if no name had been provided.