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
  • deprecated Use Evd.evar_filtered_env
  • deprecated Use Evd.evar_filtered_hyps
  • deprecated Use Evd.evar_filtered_hyps
val concl : Evd.evar_map -> goal -> EConstr.constr
  • deprecated Use Evd.evar_concl
  • deprecated Use the Refine.refine primitive and related API
val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
  • deprecated Use Refine.refine
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
  • deprecated This should be the identity now