coq/doc/sphinx/user-extensions, branch master The formal proof system Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular. 2021-04-08T12:38:21+00:00 Pierre-Marie Pédrot 2021-04-08T12:33:15+00:00 45e064836ec1f50300198f89c099b71d0e2059b9 Fixes #14092: Print Grammar ltac2 should exist. 
Fixes #14092: Print Grammar ltac2 should exist.
[abbreviation] allow the user to set arguments scope 2021-04-07T17:59:46+00:00 Enrico Tassi 2021-03-19T13:29:07+00:00 d3963fc6b6dad5a0cf79815f31b2035ca8b3de25 






Merge PR #13840: [notation] option to fine tune printing of literals
2021-03-10T13:53:55+00:00

coqbot-app[bot]

2021-03-10T13:53:55+00:00

317db327c21ac78bd921020118b19afaf1c02350

Reviewed-by: SkySkimmer
Ack-by: jfehrle





Reviewed-by: SkySkimmer
Ack-by: jfehrle







[doc] Set/Unset Printing Raw Literals
2021-03-04T15:55:14+00:00

Enrico Tassi

2021-02-09T16:15:09+00:00

edb22cd9e175b854f4caaae15a4d7489c5d06c1e












Remove decimal-only number notations
2021-02-27T11:07:39+00:00

Pierre Roux

2021-02-09T17:23:11+00:00

c02bbaeb9c6c9cbc4a7f2dc47876a94fdd33aa5e

This was deprecated in 8.12





This was deprecated in 8.12







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.







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












Merge PR #13613: [changes] mark #12765 as experimental
2020-12-14T08:33:20+00:00

coqbot-app[bot]

2020-12-14T08:33:20+00:00

d0667eb4a165c065b0d64069641ca0cd39d62219

Reviewed-by: Zimmi48





Reviewed-by: Zimmi48







Merge PR #13519: Better primitive type support in custom string and numeral notations.
2020-12-11T16:03:25+00:00

coqbot-app[bot]

2020-12-11T16:03:25+00:00

5a77078718c18b05e7ffb1366d6dd9e439ecfc91

Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer





Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer