STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530

1 files changed, 7 insertions, 0 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index d8b2de4a2..5ad1aead6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1686,6 +1686,13 @@ let collect_proof keep cur hd brkind id =
    | _ -> false in
  let may_pierce_opaque = function
    | { expr = VernacPrint (PrintName _) } -> true
+   (* These do not exactly pierce opaque, but are anyway impossible to properly
+    * delegate *)
+   | { expr = (VernacDeclareModule _
+              | VernacDefineModule _
+              | VernacDeclareModuleType _
+              | VernacInclude _) } -> true
+   | { expr =  (VernacRequire _ | VernacImport _) } -> true
    | _ -> false in
  let parent = function Some (p, _) -> p | None -> assert false in
  let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in