For printing, ordering notations by precision of the pattern.

This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion

4 files changed, 102 insertions, 11 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index bd22d45059..2cb91f26d9 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -120,14 +120,14 @@ where
 letpair x [1] = {0};
 return (1, 2, 3, 4)
      : nat * nat * nat * nat
-{{ 1 | 1 // 1 }}
-     : nat
-!!! _ _ : nat, True
-     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ((*1).2).3
      : nat
 *(1.2)
      : nat
+{{ 1 | 1 // 1 }}
+     : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ! '{{x, y}}, x.y = 0
      : Prop
 exists x : nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 839df99ea7..a98a1c5f06 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
   (let x:=a in ( .. (b0,b1) .., b2)).
 Check letpair x [1] = {0}; return (1,2,3,4).
 
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
+
 (* Test spacing in #5569 *)
 
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
@@ -191,13 +198,6 @@ Check 1+1+1.
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
 
-(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
-
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
-Check (((id 1) + 2) + 3).
-Check (id (1 + 2)).
-
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a6fd39c29b..86c4b3cccc 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected.
      : Prop
 !!!! (nat, id), nat = true /\ id = false
      : Prop
+∀ x : nat, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₂ x y, x + y = 0
+     : Prop
+((1, 2))
+     : nat * nat
+%% [x == 1]
+     : Prop
+%%% [1]
+     : Prop
+[[2]]
+     : nat * nat
+%%%
+     : Type
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 0731819bba..6af192ea82 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -414,3 +414,76 @@ Module P.
   End NotationBinderNotMixedWithTerms.
 
 End P.
+
+Module MorePrecise1.
+
+(* A notation with limited iteration is strictly more precise than a
+   notation with unlimited iteration *)
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₁ z , P" := (forall z, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₂ y x , P" := (forall y x, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+Check forall x y, x + y = 0.
+
+Notation "(( x , y ))" := (x,y) : core_scope.
+
+Check ((1,2)).
+
+End MorePrecise1.
+
+Module MorePrecise2.
+
+(* Case of a bound binder *)
+Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60).
+
+(* Case of an internal binder *)
+Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0).
+
+(* Check that the two previous notations are indeed finer *)
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀'  x  ..  y ']' ,  '/' P ']'").
+
+Check %% [x == 1].
+Check %%% [1].
+
+Notation "[[ x ]]" := (pair 1 x).
+
+Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y).
+
+(* Check which is finer *)
+Check [[ 2 ]].
+
+End MorePrecise2.
+
+Module MorePrecise3.
+
+(* This is about a binder not bound in a notation being strictly more
+   precise than a binder bound in the notation (since the notation
+   applies - a priori - stricly less often) *)
+
+Notation "%%%" := (forall x, x) (at level 0).
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+
+Check %%%.
+
+End MorePrecise3.