package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val get_current_proof_name : t -> Names.Id.t
val get_current_persistence : t -> Decl_kinds.goal_kind
val get_all_proof_names : t -> Names.Id.t list
val discard : Names.lident -> t -> t option
val discard_current : t -> t option
val give_me_the_proof : t -> Proof.t
val compact_the_proof : t -> t
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 start_proof : ontop:t option -> Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> t
val start_dependent_proof : ontop:t option -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> t
val update_global_env : t -> t
val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof
type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
val return_proof : ?allow_partial:bool -> t -> closed_proof_output
val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> closed_proof
val get_terminator : t -> proof_terminator
val set_terminator : proof_terminator -> t -> t
val get_open_goals : t -> int
val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
val set_used_variables : t -> Names.Id.t list -> (Constr.named_context * Names.lident list) * t
val get_used_variables : t -> Constr.named_context option
val get_universe_decl : t -> UState.universe_decl
val copy_terminators : src:t -> tgt:t -> t
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