package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val env : Evd.evar_map -> goal -> Environ.env
val concl : Evd.evar_map -> goal -> EConstr.constr
val extra : Evd.evar_map -> goal -> Evd.Store.t
val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
val abstract_type : Evd.evar_map -> goal -> EConstr.types