package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 : ?p:Proof.t -> 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 -> Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool
val by : unit Proofview.tactic -> bool
val use_unification_heuristics : unit -> bool
val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
val build_by_tactic : ?side_eff:bool -> Environ.env -> UState.t -> ?poly:Decl_kinds.polymorphic -> EConstr.types -> unit Proofview.tactic -> Constr.constr * bool * UState.t
val declare_implicit_tactic : unit Proofview.tactic -> unit
val clear_implicit_tactic : unit -> unit
val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option