Adapt w.r.t. rocq-prover/rocq#20060.

Author: ppedrot

src/coq_elpi_HOAS.ml

@@ -3700,9 +3700,8 @@ type module_item =
 
 [%%if coq = "8.20" || coq = "9.0"]
 type 'a generic_module_body = 'a Declarations.generic_module_body
-let module_view m = (m.Declarations.mod_mp, m.Declarations.mod_type)
+let module_view m = m.Declarations.mod_type
 let mod_type m = m.Declarations.mod_type
-let mod_mp m = m.Declarations.mod_mp
 
 let rec functor_params x =
   let open Declarations in
@@ -3711,9 +3710,8 @@ let rec functor_params x =
   | _ -> [] (* XXX non trivial functors, eg P : X with type a = nat, are badly described (no params) *)
 [%%else]
 type 'a generic_module_body = 'a Mod_declarations.generic_module_body
-let module_view m = (Mod_declarations.mod_mp m, Mod_declarations.mod_type m)
+let module_view m = Mod_declarations.mod_type m
 let mod_type = Mod_declarations.mod_type
-let mod_mp = Mod_declarations.mod_mp
 
 let rec functor_params x =
   let open Declarations in
@@ -3735,23 +3733,25 @@ let rec in_elpi_module_item ~depth path state (name, item) =
       CList.init (Array.length mind_packets) (fun i -> Gref (GlobRef.IndRef (MutInd.make2 path name,i)))
   | SFBrules _ -> nYI "rewrite rules"
   | SFBmodule b ->
+    let mod_mp = MPdot (path, name) in
     begin match module_view b with
-    | mod_mp, NoFunctor _ -> [Module (mod_mp,in_elpi_module ~depth state b) ]
-    | mod_mp, (MoreFunctor _ as l) -> [Functor(mod_mp,functor_params l)]
+    | NoFunctor _ -> [Module (mod_mp,in_elpi_module ~depth state mod_mp b) ]
+    | (MoreFunctor _ as l) -> [Functor(mod_mp,functor_params l)]
     end
   | SFBmodtype m ->
+    let mod_mp = MPdot (path, name) in
     begin match module_view m with
-    | mod_mp, NoFunctor _ -> [ModuleType mod_mp]
-    | mod_mp, (MoreFunctor _ as l) -> [FunctorType (mod_mp,functor_params l)]
+    | NoFunctor _ -> [ModuleType mod_mp]
+    | (MoreFunctor _ as l) -> [FunctorType (mod_mp,functor_params l)]
     end
 
-and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a generic_module_body -> module_item list =
-  fun ~depth state mb ->
+and in_elpi_module : 'a. depth:int -> API.Data.state -> ModPath.t -> 'a generic_module_body -> module_item list =
+  fun ~depth state mp mb ->
   match mod_type mb with
   | Declarations.MoreFunctor _ -> nYI "functors"
   | Declarations.NoFunctor contents ->
       let l =
-        CList.map (in_elpi_module_item ~depth (mod_mp mb) state) contents in
+        CList.map (in_elpi_module_item ~depth mp state) contents in
       CList.flatten l
 
 let rec in_elpi_modty_item (name, item) = match item with
@@ -3770,7 +3770,7 @@ and in_elpi_modty : 'a.'a generic_module_body -> string list =
   | Declarations.NoFunctor contents ->
       CList.flatten (CList.map in_elpi_modty_item contents)
 
-let in_elpi_module ~depth s x = in_elpi_module ~depth s x
+let in_elpi_module ~depth s mp x = in_elpi_module ~depth s mp x
 
 let in_elpi_module_type x = in_elpi_modty x
 

src/coq_elpi_HOAS.mli

@@ -269,10 +269,10 @@ type module_item =
   | FunctorType of Names.ModPath.t * Names.ModPath.t list
 
 [%%if coq = "8.20" || coq = "9.0"]
-val in_elpi_module : depth:int -> State.t -> Declarations.module_body -> module_item list
+val in_elpi_module : depth:int -> State.t -> ModPath.t -> Declarations.module_body -> module_item list
 val in_elpi_module_type : Declarations.module_type_body -> string list
 [%%else]
-val in_elpi_module : depth:int -> State.t -> Mod_declarations.module_body -> module_item list
+val in_elpi_module : depth:int -> State.t -> ModPath.t -> Mod_declarations.module_body -> module_item list
 val in_elpi_module_type : Mod_declarations.module_type_body -> string list
 [%%endif]
 

src/coq_elpi_builtins.ml

@@ -1846,7 +1846,7 @@ Supported attributes:
     Out(list module_item, "Contents",
     Read(global, "lists the contents of a module (recurses on submodules) *E*"))),
   (fun mp _ ~depth {env} _ state ->
-    let t = in_elpi_module ~depth state (Environ.lookup_module mp env) in
+    let t = in_elpi_module ~depth state mp (Environ.lookup_module mp env) in
     !: t)),
   DocAbove);