1 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index c2003816..3d4dfe60 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -110,3 +110,40 @@ 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.
+
+(* Testing a variant of #7192 across files *)
+(* This was missing in the original fix to #7192 *)
+Require Import module_bug7192.
+Print Assumptions M7192.D.f.
+
+(* Testing reporting assumptions from modules in files *)
+(* A regression introduced in the original fix to #7192 was missing implementations *)
+Require Import module_bug8416.
+Print Assumptions M8416.f.