package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val tclEVARS : Evd.evar_map -> unit tactic
val tclEVARSADVANCE : Evd.evar_map -> unit tactic
val tclSETENV : Environ.env -> unit tactic
val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic
val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
val tclSETSHELF : Evar.t list -> unit tactic
val tclGETSHELF : Evar.t list tactic
val tclPUTSHELF : Evar.t list -> unit tactic
val tclPUTGIVENUP : Evar.t list -> unit tactic
val tclEVARUNIVCONTEXT : UState.t -> unit tactic
val reset_future_goals : proofview -> proofview
val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
val mark_as_unresolvable : proofview -> Evar.t -> proofview
val advance : Evd.evar_map -> Evar.t -> Evar.t option
val typeclass_resolvable : unit Evd.Store.field