coq/doc/changelog/03-notations, branch master The formal proof system [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] changelog entry
2021-03-04T15:55:14+00:00

Enrico Tassi

2021-02-09T16:17:29+00:00

feb09c2f3ed286829f86ad31425543e6e9a9cec9












Add changelog
2021-02-27T11:07:42+00:00

Pierre Roux

2021-02-27T11:03:55+00:00

2c79e5aad6aef7204eb952b6b920f0dbafe80940












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







Better primitive type support in custom string and numeral notations.
2020-12-03T23:23:36+00:00

Fabian Kunze

2020-11-27T19:58:19+00:00

0d1da885cc8ccfb9f995e5dcb0ed79e71e6020db

- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists





- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists







[changelog] update markup
2020-12-03T15:03:37+00:00

Enrico Tassi

2020-11-30T09:03:47+00:00

c8fc6b8f0d357b01f919b8346f45d0bd020f4fe2












Changes for Coq 8.13
2020-12-03T15:03:37+00:00

Matthieu Sozeau

2020-11-30T16:12:37+00:00

3c4d2c9e3b7100a0012ad06b33b46fe7dca6cd29












Changelog for #13415
2020-11-25T12:09:35+00:00

Gaëtan Gilbert

2020-11-24T20:57:53+00:00

817c3edaf4128cdf200daa89ad4f537289744d4f












Renaming "ident" into "name" in grammar entries, to prevent confusions.
2020-11-22T12:28:40+00:00

Hugo Herbelin

2020-03-17T09:37:30+00:00

83e22b5abc05902d1468d1cf033251dae46b69bc

We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
  entries where it already meant "ident".
- "ident" will be made again available (outside situation of
  coercions) to mean "ident" at the end of deprecation phase.

Also renaming "as ident" into "as name".

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>





We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
  entries where it already meant "ident".
- "ident" will be made again available (outside situation of
  coercions) to mean "ident" at the end of deprecation phase.

Also renaming "as ident" into "as name".

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>