package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Not | `Simple of Goal.goal list ]
type !'a until = [
  1. | `Cont of 'a
  2. | `Found of Stm.static_block_declaration
  3. | `Stop
]
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