diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml index 8258affad..694d0ea2f 100644 --- 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 ->