Fixes #7192 (Print Assumptions does not enter implementation of submodules).

We fix it by looking manually for the implementation at each level of
nesting rather than using the signature for the n first levels and
looking for the implementation only in the n+1-th level.

5 files changed, 40 insertions, 7 deletions

diff --git a/library/global.ml b/library/global.ml
index 6083c4079..dcb20a280 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -259,6 +259,9 @@ let is_type_in_type r =
   | IndRef ind -> Environ.type_in_type_ind ind env
   | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
 
+let current_modpath () =
+  Safe_typing.current_modpath (safe_env ())
+
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())
 
diff --git a/library/global.mli b/library/global.mli
index 015f4d582..b82039a0c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -157,6 +157,8 @@ val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
 (* Modifies the global state, registering new universes *)
 
+val current_modpath : unit -> ModPath.t
+
 val current_dirpath : unit -> DirPath.t
 
 val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
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/vernac/assumptions.ml b/vernac/assumptions.ml
index 45ccf7276..765f962e9 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -69,16 +69,15 @@ let rec fields_of_functor f subs mp0 args = function
       fields_of_functor f subs mp0 args e
 
 let rec lookup_module_in_impl mp =
-  try Global.lookup_module mp
-  with Not_found ->
-    (* The module we search might not be exported by its englobing module(s).
-       We access the upper layer, and then do a manual search *)
     match mp with
-    | MPfile _ -> raise Not_found (* can happen if mp is an open module *)
+    | MPfile _ -> raise Not_found
     | MPbound _ -> assert false
     | MPdot (mp',lab') ->
-       let fields = memoize_fields_of_mp mp' in
-       search_mod_label lab' fields
+       if ModPath.equal mp' (Global.current_modpath ()) then
+         Global.lookup_module mp
+       else
+         let fields = memoize_fields_of_mp mp' in
+         search_mod_label lab' fields
 
 and memoize_fields_of_mp mp =
   try MPmap.find mp !modcache