package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val get_current_context : Declare.Proof.t -> Evd.evar_map * Environ.env
val solve : ?with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool
val refine_by_tactic : name:Names.Id.t -> poly:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> Constr.constr * Evd.evar_map
val build_by_tactic : ?side_eff:bool -> Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types option * bool * UState.t
val build_constant_by_tactic : name:Names.Id.t -> ?opaque:Declare.opacity_flag -> uctx:UState.t -> sign:Environ.named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic -> Evd.side_effects Declare.proof_entry * bool * UState.t
OCaml

Innovation. Community. Security.