4 files changed, 98 insertions, 0 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 66458543a..34f44cd24 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -18,3 +18,5 @@ Closed under the global context
 Closed under the global context
 Axioms:
 M.foo : False
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index c2003816c..ea1ab6378 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -110,3 +110,30 @@ End N.
 Print Assumptions N.foo.
 
 End INCLUDE.
+
+(* Print Assumptions did not enter implementation of submodules (#7192) *)
+
+Module SUBMODULES.
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module E: C.
+  Module D <: B. Definition f := a. End D.
+End E.
+Print Assumptions E.D.f.
+
+(* Idem in the scope of a functor *)
+
+Module Type T. End T.
+Module F (X : T).
+  Definition a := True.
+  Module Type B. Axiom f : Prop. End B.
+  Module Type C. Declare Module D : B. End C.
+  Module E: C.
+    Module D <: B. Definition f := a. End D.
+  End E.
+  Print Assumptions E.D.f.
+End F.
+
+End SUBMODULES.
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.