Merge PR #7771: Tweak printing boxes for unicode binders

2 files changed, 69 insertions, 0 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.