package coq

  1. Overview
  2. Docs
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 partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
val abstract_type : Evd.evar_map -> goal -> EConstr.types