coq 8.7.1 · OCaml Package

coq

val start_proof : 
  Names.Id.t ->
  ?pl:Proof_global.universe_binders ->
  Decl_kinds.goal_kind ->
  Evd.evar_map ->
  Environ.named_context_val ->
  EConstr.constr ->
  ?init_tac:unit Proofview.tactic ->
  Proof_global.proof_terminator ->
  unit

val cook_this_proof : 
  Proof_global.proof_object ->
  Names.Id.t
  * (Safe_typing.private_constants Entries.definition_entry
     * Proof_global.proof_universes
     * Decl_kinds.goal_kind)

val cook_proof : 
  unit ->
  Names.Id.t
  * (Safe_typing.private_constants Entries.definition_entry
     * Proof_global.proof_universes
     * Decl_kinds.goal_kind)

val get_goal_context : int -> Evd.evar_map * Environ.env

val get_current_goal_context : unit -> Evd.evar_map * Environ.env

val get_current_context : unit -> Evd.evar_map * Environ.env

val current_proof_statement : 
  unit ->
  Names.Id.t * Decl_kinds.goal_kind * EConstr.types

val solve : 
  ?with_end_tac:unit Proofview.tactic ->
  Vernacexpr.goal_selector ->
  int option ->
  unit Proofview.tactic ->
  Proof.proof ->
  Proof.proof * bool

val by : unit Proofview.tactic -> bool

val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit

val build_constant_by_tactic : 
  Names.Id.t ->
  Evd.evar_universe_context ->
  Environ.named_context_val ->
  ?goal_kind:Decl_kinds.goal_kind ->
  EConstr.types ->
  unit Proofview.tactic ->
  Safe_typing.private_constants Entries.definition_entry
  * bool
  * Evd.evar_universe_context

val build_by_tactic : 
  ?side_eff:bool ->
  Environ.env ->
  Evd.evar_universe_context ->
  ?poly:Decl_kinds.polymorphic ->
  EConstr.types ->
  unit Proofview.tactic ->
  Term.constr * bool * Evd.evar_universe_context

val refine_by_tactic : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  unit Proofview.tactic ->
  Term.constr * Evd.evar_map

val declare_implicit_tactic : unit Proofview.tactic -> unit

val clear_implicit_tactic : unit -> unit

val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option

val refining : unit -> bool

deprecated use Proof_global.there_are_pending_proofs

val check_no_pending_proofs : unit -> unit

deprecated use Proof_global.check_no_pending_proofs

val delete_proof : Names.Id.t Loc.located -> unit

deprecated use Proof_global.discard

val delete_current_proof : unit -> unit

deprecated use Proof_global.discard_current

val delete_all_proofs : unit -> unit

deprecated use Proof_global.discard_all

val get_pftreestate : unit -> Proof.proof

deprecated use Proof_global.give_me_the_proof

val set_end_tac : Genarg.glob_generic_argument -> unit

deprecated use Proof_global.set_endline_tactic

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

deprecated use Proof_global.set_used_variables

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

deprecated use Proof_global.get_used_variables

val get_universe_binders : unit -> Proof_global.universe_binders option

deprecated use Proof_global.get_universe_binders

val get_current_proof_name : unit -> Names.Id.t

deprecated use Proof_global.get_current_proof_name

val get_all_proof_names : unit -> Names.Id.t list

deprecated use Proof_global.get_all_proof_names

type lemma_possible_guards = Proof_global.lemma_possible_guards

deprecated use Proof_global.lemma_possible_guards

type universe_binders = Proof_global.universe_binders

deprecated use Proof_global.universe_binders

package coq