package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
type state = t
  • deprecated please use [Proof_global.t]
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
val get_current_proof_name : unit -> Names.Id.t
val get_all_proof_names : unit -> Names.Id.t list
val discard : Names.lident -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
val give_me_the_proof_opt : unit -> Proof.t option
exception NoCurrentProof
val give_me_the_proof : unit -> Proof.t
val compact_the_proof : unit -> unit
type lemma_possible_guards = int list list
type proof_object = {
  1. id : Names.Id.t;
  2. entries : Safe_typing.private_constants Entries.definition_entry list;
  3. persistence : Decl_kinds.goal_kind;
  4. universes : UState.t;
}
type opacity_flag =
  1. | Opaque
  2. | Transparent
type proof_ending =
  1. | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
  2. | Proved of opacity_flag * Names.lident option * proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
val make_terminator : (proof_ending -> unit) -> proof_terminator
val apply_terminator : proof_terminator -> proof_ending -> unit
val update_global_env : unit -> unit
val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
val close_future_proof : feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof
val get_terminator : unit -> proof_terminator
val set_terminator : proof_terminator -> unit
exception NoSuchProof
val get_open_goals : unit -> int
val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
val set_endline_tactic : Genarg.glob_generic_argument -> unit
val set_used_variables : Names.Id.t list -> Constr.named_context * Names.lident list
val get_used_variables : unit -> Constr.named_context option
val get_universe_decl : unit -> UState.universe_decl
module V82 : sig ... end
val freeze : marshallable:[ `No | `Shallow | `Yes ] -> t
val unfreeze : t -> unit
val proof_of_state : t -> Proof.t
val copy_terminators : src:t -> tgt:t -> t
type proof_mode_name = string
type proof_mode = {
  1. name : proof_mode_name;
  2. set : unit -> unit;
  3. reset : unit -> unit;
}
val register_proof_mode : proof_mode -> unit
val proof_mode_opt_name : string list
val get_default_proof_mode_name : unit -> proof_mode_name
  • deprecated the current proof mode API is deprecated, use with care, see PR #459 and #566
val set_proof_mode : proof_mode_name -> unit
  • deprecated the current proof mode API is deprecated, use with care, see PR #459 and #566
val activate_proof_mode : proof_mode_name -> unit
  • deprecated the current proof mode API is deprecated, use with care, see PR #459 and #566
val disactivate_current_proof_mode : unit -> unit
  • deprecated the current proof mode API is deprecated, use with care, see PR #459 and #566