Module `ProofBlockDelimiter`

val simple_goal : Evd.evar_map -> Evar.t -> Evar.t list -> bool: A goal is simple if it nor depends on nor impacts on any other goal. This function is used to detect, dynamically, if a proof block leaks, i.e. if skipping it could impact other goals (like not instantiating their type). `Simple carries the list of focused goals.

val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Evar.t list | `Not ]

type 'a until = [ | `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]

val crawl : Stm.document_view -> ?⁠init:Stm.document_node option -> ('a -> Stm.document_node -> 'a until) -> 'a -> Stm.static_block_declaration option
val unit_val : Stm.DynBlockData.t
val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t