package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception UnableToUnify of Evd.evar_map * Pretype_errors.unification_error
  • deprecated Use [Evarconv.conv]
  • deprecated Use [Evarconv.cumul]
val solve_unif_constraints_with_heuristics : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map -> Evd.evar_map
val consider_remaining_unif_problems : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map -> Evd.evar_map
  • deprecated Alias for [solve_unif_constraints_with_heuristics]
val check_problems_are_solved : Environ.env -> Evd.evar_map -> unit
val set_solve_evars : (Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr) -> unit
val set_evar_conv : unify_fun -> unit
val evar_conv_x : unify_fun