diff options
| author | Hugo Herbelin | 2019-11-23 22:37:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-03 21:22:03 +0100 |
| commit | 19b2b4389b75a7701b62c5a67d9117a72656dab3 (patch) | |
| tree | 202dd76ca90428fc6eea9f62c1b773b8fd290489 /doc | |
| parent | effbc03b9072ff94f96e54a5026ce04d7aa41bcc (diff) | |
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.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst | 1 |
1 files changed, 1 insertions, 0 deletions
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 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). |