3 files changed, 46 insertions, 16 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 838ef40545..70ce6cef19 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -716,20 +716,20 @@ let rec flatten_application c = match DAst.get c with
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token (custom,scopes) r =
-  try
-    let (sc,n) = uninterp_prim_token r in
-    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-    | None -> raise No_match
-    | Some coercion ->
-    match availability_of_prim_token n sc scopes with
-    | None -> None
-    | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key))
-  with No_match ->
-    None
-
-let extern_optimal_prim_token scopes r r' =
-  let c = extern_possible_prim_token scopes r in
-  let c' = if r==r' then None else extern_possible_prim_token scopes r' in
+   let (sc,n) = uninterp_prim_token r in
+   match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+   | None -> raise No_match
+   | Some coercion ->
+   match availability_of_prim_token n sc scopes with
+   | None -> raise No_match
+   | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+
+let extern_possible extern r =
+  try Some (extern r) with No_match -> None
+
+let extern_optimal extern r r' =
+  let c = extern_possible extern r in
+  let c' = if r==r' then None else extern_possible extern r' in
   match c,c' with
   | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
   | _ -> raise No_match
@@ -769,12 +769,14 @@ let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_optimal_prim_token scopes r r'
+    extern_optimal (extern_possible_prim_token scopes) r r'
   with No_match ->
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_notation scopes vars r'' (uninterp_notations r'')
+    extern_optimal
+      (fun r -> extern_notation scopes vars r (uninterp_notations r))
+      r r''
   with No_match ->
   let loc = r'.CAst.loc in
   match DAst.get r' with
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.