coq 8.7.1+1 · OCaml Package

coq

val parse_sentence : 
  Stateid.t ->
  Pcoq.Gram.coq_parsable ->
  Vernacexpr.vernac_expr Loc.located

exception End_of_input

val add : 
  ontop:Stateid.t ->
  ?newtip:Stateid.t ->
  bool ->
  Vernacexpr.vernac_expr Loc.located ->
  Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]

val query : 
  at:Stateid.t ->
  route:Feedback.route_id ->
  Pcoq.Gram.coq_parsable ->
  unit

type focus = {

start : Stateid.t;
stop : Stateid.t;
tip : Stateid.t;

}

val edit_at : Stateid.t -> [ `Focus of focus | `NewTip ]

val finish : unit -> unit

val observe : Stateid.t -> unit

val stop_worker : string -> unit

val join : unit -> unit

val snapshot_vio : Names.DirPath.t -> string -> unit

val reset_task_queue : unit -> unit

type tasks

val check_task : string -> tasks -> int -> bool

val info_tasks : tasks -> (string * float * int) list

val finish_tasks : 
  string ->
  Library.seg_univ ->
  Library.seg_discharge ->
  Library.seg_proofs ->
  tasks ->
  Library.seg_univ * Library.seg_proofs

val get_current_state : unit -> Stateid.t

val init : unit -> unit

val get_ast : Stateid.t -> Vernacexpr.vernac_expr Loc.located option

val set_compilation_hints : string -> unit

val set_perspective : Stateid.t list -> unit

type document

val backup : unit -> document

val restore : document -> unit

module ProofTask : AsyncTaskQueue.Task

module TacTask : AsyncTaskQueue.Task

module QueryTask : AsyncTaskQueue.Task

module DynBlockData : Dyn.S

type static_block_declaration = {

block_start : Stateid.t;
block_stop : Stateid.t;
dynamic_switch : Stateid.t;
carry_on_data : DynBlockData.t;

}

type document_node = {

indentation : int;
ast : Vernacexpr.vernac_expr;
id : Stateid.t;

}

type document_view = {

entry_point : document_node;
prev_node : document_node -> document_node option;

}

type static_block_detection = document_view -> static_block_declaration option

type recovery_action = {

base_state : Stateid.t;
goals_to_admit : Goal.goal list;
recovery_command : Vernacexpr.vernac_expr option;

}

type dynamic_block_error_recovery =
  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 : (Stateid.t -> in_cache:bool -> unit) Hook.t

val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t

val state_ready_hook : (Stateid.t -> unit) Hook.t

val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t

type state = {

system : States.state;
proof : Proof_global.state;
shallow : bool;

}

val state_of_id : 
  Stateid.t ->
  [ `Error of exn | `Expired | `Valid of state option ]

val current_proof_depth : unit -> int

val get_all_proof_names : unit -> Names.Id.t list

package coq