2 files changed, 0 insertions, 11 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 593a5df84c..6ff1d38372 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,7 +54,3 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
-fun x : nat => (## x) + x
-     : nat -> nat
-fun x : nat => ## x + x
-     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index d32758375f..4e0d135d7d 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,10 +106,3 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
-
-(* Check printing of notations that have arguments at higher level
-   than the notation itself *)
-
-Notation "## a" := (S a) (at level 0, a at level 100).
-Check fun x => (S x) + x.
-Check fun x => S (x + x).