package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val normalize : t -> t tactic
val concl : t -> EConstr.constr
val hyps : t -> EConstr.named_context
val env : t -> Environ.env
val sigma : t -> Evd.evar_map
val extra : t -> Evd.Store.t
val nf_enter : (t -> unit tactic) -> unit tactic
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 -> Goal.goal Evd.sigma
OCaml

Innovation. Community. Security.