From 37bab241c737e27a02464118abac81ba4296c0eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 15 Jan 2025 15:15:57 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#20060. --- template-coq/src/plugin_core.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 ->