package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
val tactic : ?nf_evars:bool -> tac -> unit tactic
val nf_evar_goals : unit tactic
val has_unresolved_evar : proofview -> bool
val grab : proofview -> proofview
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
val top_evars : entry -> proofview -> Evar.t list
val of_tactic : 'a tactic -> tac
val put_status : bool -> unit tactic
val catchable_exception : exn -> bool
val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic