2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 28621ccd81..6e59c36777 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -127,3 +127,8 @@ fun x : list ?99 => match x with
      : list ?99 -> option (list ?99)
 s
      : s
+Identifier 'foo' now a keyword
+10
+     : nat
+fun _ : nat => 9
+     : nat -> nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index d5763022e8..75d5037a85 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -257,3 +257,12 @@ Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end).
 
 Notation s := Type.
 Check s.
+
+(* Test bug #2835: notations were not uniformly managed under prod and lambda *)
+
+Open Scope nat_scope.
+
+Notation "'foo' n" := (S n) (at level 50): nat_scope.
+
+Check (foo 9).
+Check (fun _ : nat => 9).