Merge PR coq#18511: Forbid opening a functor with Import

Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Frigory33 · Jan 19, 2024 · b8ba7d6 · b8ba7d6
2 parents 49680bc + 6b2218f
commit b8ba7d6
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/test-suite/bugs/bug_18504.v b/test-suite/bugs/bug_18504.v
@@ -0,0 +1,12 @@
+Module Type SIG.
+End SIG.
+
+Fail Module Import A (S:SIG).
+
+Module Type F(X:SIG). End F.
+
+Fail Declare Module Import M : F.
+
+Declare Module M : F.
+
+Fail Module Import N := M.
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
@@ -776,6 +776,9 @@ let start_module_core id args res =
   mp, res_entry_o, mbids, sign, args
 
 let start_module export id args res =
+  let () = if Option.has_some export && not (CList.is_empty args)
+    then user_err Pp.(str "Cannot import functors.")
+  in
   let fs = Summary.Synterp.freeze_summaries () in
   let mp, res_entry_o, mbids, sign, args = start_module_core id args res in
   set_openmod_syntax_info { cur_mp = mp; cur_typ = res_entry_o; cur_mbids = mbids };