Merge pull request #1134 from ppedrot/module-remove-modpath

Adapt w.r.t. coq/coq#20060.
MetaCoq · Jan 15, 2025 · f827908 · f827908
2 parents fef51be + 37bab24
commit f827908
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -197,12 +197,12 @@ let quote_module ~(include_functor : bool) ~(include_submodule : bool) ~(include
           | SFBconst _ -> [GlobRef.ConstRef (Constant.make2 mp label)]
           | SFBmind _ -> [GlobRef.IndRef (MutInd.make2 mp label, 0)]
           | SFBrules _ -> failwith "Rewrite rules are not supported by TemplateCoq"
-          | SFBmodule mb -> if include_submodule then aux (mod_type mb) (mod_mp mb) else []
-          | SFBmodtype mtb -> if include_submodtype then aux (mod_type mtb) (mod_mp mtb) else []
+          | SFBmodule mb -> if include_submodule then aux (mod_type mb) (MPdot (mp, label)) else []
+          | SFBmodtype mtb -> if include_submodtype then aux (mod_type mtb) (MPdot (mp, label)) else []
         in
         CList.map_append get_ref body
     in aux' mb mp
-  in aux (mod_type mb) (mod_mp mb)
+  in aux (mod_type mb) mp
 
 let tmQuoteModule (qualid : qualid) : global_reference list tm =
   fun ~st env evd success _fail ->