From c90e2d81ee0dc5198176300f0140a9e0a71a4cc5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 25 Sep 2018 12:53:45 +0200
Subject: Using scope for printing: more tests.

---
 test-suite/output/Notations4.out |  8 ++++++++
 test-suite/output/Notations4.v   | 16 ++++++++++++++++
 2 files changed, 24 insertions(+)

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index acd69f3f50..2ff21f6a57 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -23,3 +23,11 @@ Let "x" e1 e2
      : expr
 fun x : nat => (# x)%nat
      : nat -> nat
+fun x : nat => ## x
+     : nat -> nat
+fun x : nat => # x
+     : nat -> nat
+fun x : nat => ### x
+     : nat -> nat
+fun x : nat => ## x
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 12e98c3d64..4720cb0561 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -106,3 +106,19 @@ Notation "# x" := (Some x).
 Check fun x => (# x)%nat.
 
 End E.
+
+(* Other tests of precedence *)
+
+Module F.
+
+Notation "# x" := (S x) (at level 20) : nat_scope.
+Notation "## x" := (S x) (at level 20).
+Check fun x => S x.
+Open Scope nat_scope.
+Check fun x => S x.
+Notation "### x" := (S x) (at level 20) : nat_scope.
+Check fun x => S x.
+Close Scope nat_scope.
+Check fun x => S x.
+
+End F.
-- 
cgit v1.2.3