From 4c39126f0a0a97152f67a3a5e7c86db860f48e39 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 24 Apr 2020 21:52:37 +0200 Subject: Fix #12159 (Numeral Notations do not play well with multiple scopes for the 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) --- doc/changelog/03-notations/12163-fix-12159.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 doc/changelog/03-notations/12163-fix-12159.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst new file mode 100644 index 0000000000..978ed561dd --- /dev/null +++ b/doc/changelog/03-notations/12163-fix-12159.rst @@ -0,0 +1,11 @@ +- **Fixed:** + Numeral Notations now play better with multiple scopes for the same + inductive type. Previously, when multiple numeral notations were defined + for the same inductive, only the last one was considered for + printing. Now, among the notations that are usable for printing and either + have a scope delimiter or are open, the selection is made according + to the order of open scopes, or according to the last defined + notation if no appropriate scope is open + (`#12163 `_, + fixes `#12159 `_, + by Pierre Roux, review by Hugo Herbelin and Jason Gross). -- cgit v1.2.3