Tweak printing boxes for unicode binders

3 files changed, 72 insertions, 3 deletions

diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out
new file mode 100644
index 000000000..a57b3bbad
--- /dev/null
+++ b/test-suite/output/Unicode.out
@@ -0,0 +1,41 @@
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+        f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
+        (z : very_very_long_type_name2), f y x ∧ f y z
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
+        (z : very_very_long_type_name2),
+        f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∃ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+        f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
diff --git a/test-suite/output/Unicode.v b/test-suite/output/Unicode.v
new file mode 100644
index 000000000..42b07e5a0
--- /dev/null
+++ b/test-suite/output/Unicode.v
@@ -0,0 +1,28 @@
+Require Import Coq.Unicode.Utf8.
+
+Section test.
+Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type).
+Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop).
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+         (z : very_very_long_type_name2),
+    f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+         (z : very_very_long_type_name2),
+    f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  exists (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+End test.
diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v
index 5a8931a8c..d4cdb064f 100644
--- a/theories/Unicode/Utf8_core.v
+++ b/theories/Unicode/Utf8_core.v
@@ -14,10 +14,10 @@
 (* Logic *)
 Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
   (at level 200, x binder, y binder, right associativity,
-  format "'[  ' ∀  x  ..  y ']' ,  P") : type_scope.
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
 Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
   (at level 200, x binder, y binder, right associativity,
-  format "'[  ' ∃  x  ..  y ']' ,  P") : type_scope.
+  format "'[  ' '[  ' ∃  x  ..  y ']' ,  '/' P ']'") : type_scope.
 
 Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
 Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
@@ -31,4 +31,4 @@ Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
 (* Abstraction *)
 Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
   (at level 200, x binder, y binder, right associativity,
-  format "'[  ' 'λ'  x  ..  y ']' ,  t").
+  format "'[  ' '[  ' 'λ'  x  ..  y ']' ,  '/' t ']'").