package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val concl : t -> EConstr.constr
val hyps : t -> EConstr.named_context
val env : t -> Environ.env
val sigma : t -> Evd.evar_map
val nf_enter : (t -> unit tactic) -> unit tactic
  • deprecated Normalization is enforced by EConstr, please use [enter]
val enter : (t -> unit tactic) -> unit tactic
val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
val goals : t tactic list tactic
val unsolved : t -> bool tactic
val goal : t -> Evar.t
val print : t -> Evar.t Evd.sigma