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.
---
 test-suite/output/Notations4.out | 2 ++
 test-suite/output/Notations4.v   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 32120a9674..799d310fa7 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,6 +31,8 @@ Let "x" e1 e2
      : expr
 Let "x" e1 e2
      : expr
+Let "x" e1 e2 : list string
+     : list string
 myAnd1 True True
      : Prop
 r 2 3
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d3433949d1..26c7840a16 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -94,6 +94,10 @@ Coercion App : expr >-> Funclass.
 
 Check (Let "x" e1 e2).
 
+Axiom free_vars :> expr -> list string.
+
+Check (Let "x" e1 e2) : list string.
+
 End D.
 
 (* Fixing bugs reported by G. Gonthier in #9207 *)
-- 
cgit v1.2.3