6 files changed, 32 insertions, 6 deletions
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index bd9240476f..b67ac4f0df 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -10,6 +10,8 @@ Arguments Nat.sub !n !m.
 About Nat.sub.
 Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
   fun x => (f (fst x), g (snd x)).
+Declare Scope foo_scope.
+Declare Scope bar_scope.
 Delimit Scope foo_scope with F.
 Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
 About pf.
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39e..adab324cf0 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -76,6 +76,7 @@ Open Scope nat_scope.
 Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
 Coercion Zpos: nat >-> znat.
 
+Declare Scope znat_scope.
 Delimit Scope znat_scope with znat.
 Open Scope znat_scope.
 
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 34f44cd246..3f4d5ef58c 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -20,3 +20,5 @@ Axioms:
 M.foo : False
 Closed under the global context
 Closed under the global context
+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 ea1ab63786..3d4dfe603d 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -137,3 +137,13 @@ Module F (X : T).
 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.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 6f41b2fcf9..926114a1e1 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -48,6 +48,12 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
+Type@{i} -> Type@{j}
+     : Type@{max(i+1,j+1)}
+(* {j i} |=  *)
+     = Type@{i} -> Type@{j}
+     : Type@{max(i+1,j+1)}
+(* {j i} |=  *)
 Monomorphic mono = Type@{mono.u}
      : Type@{mono.u+1}
 (* {mono.u} |=  *)
@@ -149,24 +155,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i}
-(* i Top.44 Top.45 |=  *)
+axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i}
-(* i Top.44 Top.45 |=  *)
+axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.47} -> Type@{axbar'.i}
+axfoo' : Type@{Top.51} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.47} -> Type@{axbar'.i}
+axbar' : Type@{Top.51} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index c6efc240a6..f806a9f4f7 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -30,6 +30,11 @@ Unset Strict Universe Declaration.
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+
+Check Type@{i} -> Type@{j}.
+
+Eval cbv in Type@{i} -> Type@{j}.
+
 Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)