aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/03-notations
AgeCommit message (Collapse)Author
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
2021-03-04[doc] changelog entryEnrico Tassi
2021-02-27Add changelogPierre Roux
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: proux01 Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
- 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
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-25Changelog for #13415Gaëtan Gilbert
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
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>
2020-11-20Add changelog for #13265.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions ↵coqbot-app[bot]
between variable and non-qualified global references Reviewed-by: ejgallego Ack-by: maximedenes Ack-by: gares
2020-11-20Update ↵Hugo Herbelin
doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ↵coqbot-app[bot]
then by last imported Reviewed-by: Zimmi48 Ack-by: RalfJung Ack-by: gares
2020-11-18Adding change log for #12765.Hugo Herbelin
2020-11-17Adding change log for #12984.Hugo Herbelin
Co-authored-by: Ralf Jung <post@ralfj.de>
2020-11-17Add changelog for #12986.Hugo Herbelin
2020-11-16Add change log for #12965.Hugo Herbelin
2020-11-15Adding change log for #12685.Hugo Herbelin
2020-11-05Added change log for #12099.Hugo Herbelin
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Add changelogPierre Roux
2020-10-19Adding change log for #13092.Hugo Herbelin
2020-10-10Adding change log for #12950.Hugo Herbelin
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a ↵coqbot-app[bot]
lonely notation at printing time. Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested ↵coqbot-app[bot]
applications in notations Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-15Adding change log for #13026.Hugo Herbelin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-02Adding change log for #12960.Hugo Herbelin
2020-09-02Adding change log for #12946.Hugo Herbelin
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-12Adding change log.Hugo Herbelin
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-13Adding change log for #8808.Hugo Herbelin
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the ↵Pierre Roux
same inductive) Numeral Notations now play better with multiple scopes for the same inductive. Previously, when multiple numeral notations where defined for the same inductive, only the last one was considered for printing. Now, we proceed as follows 1. keep only uninterpreters that produce an output (first List.map_filter) 2. keep only uninterpretation for scopes that either have a scope delimiter or are open (second List.map_filter) 3. the final selection is made according to the order of open scopes, (find_uninterpretation) or or according to the last defined notation if no appropriate scope is open (head of list at the end)
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-03Adding changelog for 8.11.1.Pierre-Marie Pédrot
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25Update changelogPierre Roux
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:21:46 +0000