package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module AsyncOpts : sig ... end
type stm_doc_type =
  1. | VoDoc of string
  2. | VioDoc of string
  3. | Interactive of Names.DirPath.t
type stm_init_options = {
  1. doc_type : stm_doc_type;
  2. iload_path : Mltop.coq_path list;
  3. require_libs : (string * string option * bool option) list;
  4. stm_options : AsyncOpts.stm_opt;
}
type doc
val init_core : unit -> unit
val new_doc : stm_init_options -> doc * Stateid.t
exception End_of_input
val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
val query : doc:doc -> at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
type focus = {
  1. start : Stateid.t;
  2. stop : Stateid.t;
  3. tip : Stateid.t;
}
val edit_at : doc:doc -> Stateid.t -> doc * [ `Focus of focus | `NewTip ]
val observe : doc:doc -> Stateid.t -> doc
val finish : doc:doc -> doc
val wait : doc:doc -> doc
val stop_worker : string -> unit
val join : doc:doc -> doc
val snapshot_vio : doc:doc -> Names.DirPath.t -> string -> doc
val reset_task_queue : unit -> unit
type tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
val get_current_state : doc:doc -> Stateid.t
val get_ldir : doc:doc -> Names.DirPath.t
val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located option
val set_compilation_hints : string -> unit
val set_perspective : doc:doc -> Stateid.t list -> unit
type static_block_declaration = {
  1. block_start : Stateid.t;
  2. block_stop : Stateid.t;
  3. dynamic_switch : Stateid.t;
  4. carry_on_data : DynBlockData.t;
}
type document_node = {
  1. indentation : int;
  2. ast : Vernacexpr.vernac_control;
  3. id : Stateid.t;
}
type document_view = {
  1. entry_point : document_node;
  2. prev_node : document_node -> document_node option;
}
type static_block_detection = document_view -> static_block_declaration option
type recovery_action = {
  1. base_state : Stateid.t;
  2. goals_to_admit : Goal.goal list;
  3. recovery_command : Vernacexpr.vernac_control option;
}
type dynamic_block_error_recovery = doc -> static_block_declaration -> [ `Leaks | `ValidBlock of recovery_action ]
val register_proof_block_delimiter : Vernacexpr.proof_block_name -> static_block_detection -> dynamic_block_error_recovery -> unit
val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t
val unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
val get_doc : Feedback.doc_id -> doc
val state_of_id : doc:doc -> Stateid.t -> [ `Error of exn | `Expired | `Valid of Vernacstate.t option ]
val current_proof_depth : doc:doc -> int
val get_all_proof_names : doc:doc -> Names.Id.t list
val stm_debug : bool ref
type document
val backup : unit -> document
val restore : document -> unit