package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a declaration_hook
val set_start_hook : (EConstr.types -> unit) -> unit
val start_proof_com : ?inference_hook:Pretyping.inference_hook -> Decl_kinds.goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit
val start_proof_with_initialization : Decl_kinds.goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Names.Id.t * (EConstr.types * (Names.Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit
val universe_proof_terminator : Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator
val fresh_name_for_anonymous_theorem : unit -> Names.Id.t
val set_save_hook : (Proof.t -> unit) -> unit
val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
val get_current_context : unit -> Evd.evar_map * Environ.env
  • deprecated please use [Pfedit.get_current_context]