coq 8.7.2 · OCaml Package

coq

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.Id.t Loc.located -> unit

val discard_current : unit -> unit

val discard_all : unit -> unit

exception NoCurrentProof

val give_me_the_proof : unit -> Proof.proof

val compact_the_proof : unit -> unit

type lemma_possible_guards = int list list

type proof_universes =
  Evd.evar_universe_context * Universes.universe_binders option

type universe_binders = Names.Id.t Loc.located list

type proof_object = {

id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
universes : proof_universes;

}

type proof_ending =

| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag * Vernacexpr.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 : 
  Evd.evar_map ->
  Names.Id.t ->
  ?pl:universe_binders ->
  Decl_kinds.goal_kind ->
  (Environ.env * EConstr.types) list ->
  proof_terminator ->
  unit

val start_dependent_proof : 
  Names.Id.t ->
  ?pl:universe_binders ->
  Decl_kinds.goal_kind ->
  Proofview.telescope ->
  proof_terminator ->
  unit

val update_global_env : unit -> unit

val close_proof : 
  keep_body_ucst_separate:bool ->
  Future.fix_exn ->
  closed_proof

type closed_proof_output =
  (Term.constr * Safe_typing.private_constants) list
  * Evd.evar_universe_context

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.proof -> Proof.proof * 'a) ->
  'a

val simple_with_current_proof : 
  (unit Proofview.tactic -> Proof.proof -> Proof.proof) ->
  unit

val set_endline_tactic : Genarg.glob_generic_argument -> unit

val set_used_variables : 
  Names.Id.t list ->
  Context.Named.t * Names.Id.t Loc.located list

val get_used_variables : unit -> Context.Named.t option

val get_universe_binders : unit -> universe_binders option

module Bullet : sig ... end

val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds

val get_default_goal_selector : unit -> Vernacexpr.goal_selector

module V82 : sig ... end

type state

val freeze : marshallable:[ `No | `Shallow | `Yes ] -> state

val unfreeze : state -> unit

val proof_of_state : state -> Proof.proof

val copy_terminators : src:state -> tgt:state -> state

type proof_mode_name = string

type proof_mode = {

name : proof_mode_name;
set : unit -> unit;
reset : unit -> unit;

}

val register_proof_mode : proof_mode -> unit

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

package coq