package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type 'a t

val assume : 'a t -> [ `NF ] t

val normalize : 'a t -> [ `NF ] t tactic

val concl : 'a t -> EConstr.constr

val hyps : 'a t -> EConstr.named_context

val env : 'a t -> Environ.env

val sigma : 'a t -> Evd.evar_map

val extra : 'a t -> Evd.Store.t

val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic

val enter : ([ `LZ ] t -> unit tactic) -> unit tactic

val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic

val goals : [ `LZ ] t tactic list tactic

val unsolved : 'a t -> bool tactic

val goal : [ `NF ] t -> Evar.t