aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/03-notations
AgeCommit message (Collapse)Author
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
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-24added changelogAbhishek Anand (optiplex7010@home)
2020-02-23Addressing a changelog comment from Théo Zimmermann.Hugo Herbelin
2020-02-23Update ↵Hugo Herbelin
doc/changelog/03-notations/11120-master+refactoring-application-printing.rst Thanks Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-23Apply and generalize suggestions from Théo.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-22Adding a changelog item.Hugo Herbelin
2020-02-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-16Adding change log.Hugo Herbelin
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still ↵Emilio Jesus Gallego Arias
missing them. Reviewed-by: ejgallego
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
Reviewed-by: herbelin Ack-by: jfehrle
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Fix typo in changelog entry.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2019-12-26Add rew dependent NotationsJason Gross
This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too.
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
Fixes #9532 Fixes #9490
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-03Update ↵Hugo Herbelin
doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
We renounce to the ad hoc rule preferring a notation w/o delimiter for a term with coercions stripped over a notation for the fully-applied terms with coercions not removed. Instead, we interleave removal of coercions and search for notations: we prefer a notation for the fully applied term, and, if not, try to remove one coercion, and try again a notation for the remaining term, and if not, try to remove the next coercion, etc. Note: the flatten_application could be removed if prim_token were able to apply on a prefix of an application node.
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-11-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now.
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation ↵Hugo Herbelin
regression).
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
We restrict #8890 so that it looks for a notation only for the fully applied coercion.
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-28Fix typos.Théo Zimmermann
Co-Authored-By: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com>
2019-10-28Add changelog for #10963.Théo Zimmermann
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-05-13Move last changelog entries for 8.10+beta1.Théo Zimmermann
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 22:34:58 +0000