Notations: Trying using a notation with or w/o removal of coercions.

Preferring a notation which does require a delimiter, depending on
whether the coercion is removed or not, was done for primitive tokens.

We do it for all notations.

2 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 46784d1897..d25ad5dca8 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -17,3 +17,7 @@ end
      : Expr -> Expr
 [(1 + 1)]
      : Expr
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2
+     : expr
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6bdbf1bed5..7800e91ee5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -70,3 +70,27 @@ Notation "( x )" := x (in custom expr at level 0, x at level 2).
 Check [1 + 1].
 
 End C.
+
+(* An example of interaction between coercion and notations from
+   Robbert Krebbers. *)
+
+Require Import String.
+
+Module D.
+
+Inductive expr :=
+  | Var : string -> expr
+  | Lam : string -> expr -> expr
+  | App : expr -> expr -> expr.
+
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+
+Parameter e1 e2 : expr.
+
+Check (Let "x" e1 e2).
+
+Coercion App : expr >-> Funclass.
+
+Check (Let "x" e1 e2).
+
+End D.