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
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