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 tclNEWSHELVED : Evar.t list -> unit tactic
val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
val tclGETSHELF : Evar.t list tactic
val tclEVARUNIVCONTEXT : UState.t -> unit tactic
val push_future_goals : proofview -> proofview
val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
val mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map
val mark_as_unresolvables : proofview -> Evar.t list -> proofview
val advance : Evd.evar_map -> Evar.t -> Evar.t option
val update_sigma_univs : UGraph.t -> proofview -> proofview