From 8f7c82b8a67a3c94073e55289996f02285c04914 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Oct 2018 15:50:28 +0200
Subject: Printing priority to most recent notation in case of non-open scopes
 with delim.

This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.

Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
---
 test-suite/output/Notations4.out |  2 ++
 test-suite/output/Notations4.v   | 14 ++++++++++++++
 2 files changed, 16 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 2ff21f6a57..40d875e8ab 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,3 +31,5 @@ fun x : nat => ### x
      : nat -> nat
 fun x : nat => ## x
      : nat -> nat
+fun x : nat => (x.-1)%pred
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4720cb0561..4196c7e6b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -122,3 +122,17 @@ Close Scope nat_scope.
 Check fun x => S x.
 
 End F.
+
+(* Lower priority of generic application rules *)
+
+Module G.
+
+Declare Scope predecessor_scope.
+Delimit Scope predecessor_scope with pred.
+Declare Scope app_scope.
+Delimit Scope app_scope with app.
+Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope.
+Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope.
+Check fun x => pred x.
+
+End G.
-- 
cgit v1.2.3