A (significant) simplification in printing notations with recursive binders.

For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.

We let the general case absorb this particular case.

We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).

Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?

4 files changed, 13 insertions, 8 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 121a369a9..0e5f39903 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -17,10 +17,8 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
 ∃ n p : nat, n + p = 0
      : Prop
 let a := 0 in
-∃ x y : nat,
-let b := 1 in
-let c := b in
-let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
+∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), 
+x + y = z + d
      : Prop
 ∀ n p : nat, n + p = 0
      : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 531398bb0..923caedac 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x).
 
 (* Test notations with binders *)
 
-Notation "∃  x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
-  (x binder, y binder, at level 200, right associativity).
+Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
+  (x binder, y binder, at level 200, right associativity,
+  format "'[  ' ∃  x  ..  y ']' ,  P").
 
 Check (∃ n p, n+p=0).
 
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 7c47c0885..cb18fa356 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -152,8 +152,7 @@ exists x : nat,
     nat ->
     exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
      : Prop
-exists_true '{{x, y}},
-(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0)
+exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0
      : Prop
 exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
 (forall x : A, R x x)
@@ -173,6 +172,8 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop * Prop
 exists_non_null x y z t : nat , x = y /\ z = t
      : Prop
+forall_non_null x y z t : nat , x = y /\ z = t
+     : Prop
 {{RL 1, 2}}
      : nat * (nat * nat)
 {{RR 1, 2}}
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ee6f0a09e..d768b9ba4 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -308,6 +308,11 @@ Notation "'exists_non_null' x .. y  , P" :=
   (at level 200, x binder).
 Check exists_non_null x y z t , x=y/\z=t.
 
+Notation "'forall_non_null' x .. y  , P" :=
+  (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..)
+  (at level 200, x binder).
+Check forall_non_null x y z t , x=y/\z=t.
+
 (* Examples where the recursive pattern is in reverse order *)
 
 Notation "{{RL  c , .. , d }}" := (pair d .. (pair c 0) ..).