From 19b2b4389b75a7701b62c5a67d9117a72656dab3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Nov 2019 22:37:42 +0100 Subject: Printing: Interleaving search for notations and removal of coercions. 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. --- .../03-notations/11172-master+coercion-notation-interleaved-printing.rst | 1 + 1 file changed, 1 insertion(+) create mode 100644 doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst new file mode 100644 index 0000000000..5f279fc9ba --- /dev/null +++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst @@ -0,0 +1 @@ +- In printing, now interleave search for notations and removal of coercions (`#11172 `_, by Hugo Herbelin). -- cgit v1.2.3