Merge PR #8417: Fixing #8416: Print Assumptions missing module information from compiles files

6 files changed, 26 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index b8aac8b6f8..f5ec80bcfc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
-  prerequisite/bind_univs.v.log
+  prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \
+  prerequisite/module_bug7192.v.log
 
 #######################################################################
 # Phony targets
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/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v
new file mode 100644
index 0000000000..82cfe560af
--- /dev/null
+++ b/test-suite/prerequisite/module_bug7192.v
@@ -0,0 +1,9 @@
+(* Variant of #7192 to be tested in a file requiring this file *)
+(* #7192 is about Print Assumptions not entering implementation of submodules *)
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module M7192: C.
+  Module D <: B. Definition f := a. End D.
+End M7192.
diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v
new file mode 100644
index 0000000000..70f43d132a
--- /dev/null
+++ b/test-suite/prerequisite/module_bug8416.v
@@ -0,0 +1,2 @@
+Module Type A. Axiom f : True. End A.
+Module M8416 : A. Definition f := I. End M8416.
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 765f962e99..e5d2382e46 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function
 
 let rec lookup_module_in_impl mp =
     match mp with
-    | MPfile _ -> raise Not_found
+    | MPfile _ -> Global.lookup_module mp
     | MPbound _ -> assert false
     | MPdot (mp',lab') ->
        if ModPath.equal mp' (Global.current_modpath ()) then