Taking into account binding patterns when agglutinating sequences of binders.

Supporting accordingly printing of sequences of binders including binding
patterns.

3 files changed, 27 insertions, 1 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 950382d572..360f379676 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -96,3 +96,5 @@ fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
      : nat -> Prop
 fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+     : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9efac6508c..4b8bfe3124 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -115,3 +115,27 @@ Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
 Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
 Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
 
+(**********************************************************************)
+(* Test printing of #4932                                             *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (fun x => .. (fun z =>
+     pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+          (existT _ x .. (existT _ z tt) .. )
+                ) ..)
+  (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 5f9ea9e3d6..6acaa0ccec 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -23,7 +23,7 @@ Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
 forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
      : Prop
-exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+exists '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
 fun pat : nat * nat =>