diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 7 |
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 |