package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module AsyncOpts : sig ... end
type interactive_top =
  1. | TopLogical of Names.DirPath.t
  2. | TopPhysical of string
type stm_doc_type =
  1. | VoDoc of string
  2. | VioDoc of string
  3. | Interactive of interactive_top
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
val parse_sentence : doc:doc -> Stateid.t -> entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
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 -> output_native_objects:bool -> 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 : Vernacextend.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 document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t
val document_edit_hook : (Stateid.t -> unit) Hook.t
val sentence_exec_hook : (Stateid.t -> 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct