package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type unify_flags = Evarsolve.unify_flags
val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags
val conv_fun : unify_fun -> Evarsolve.unifier
exception UnableToUnify of Evd.evar_map * Pretype_errors.unification_error
val unify : ?flags:unify_flags -> ?with_ho:bool -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> Evd.evar_map
val solve_unif_constraints_with_heuristics : Environ.env -> ?flags:unify_flags -> ?with_ho:bool -> Evd.evar_map -> Evd.evar_map
val check_problems_are_solved : Environ.env -> Evd.evar_map -> unit
type occurrence_match_test = Environ.env -> Evd.evar_map -> EConstr.constr -> Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.constr -> bool * Evd.evar_map
type occurrence_selection =
  1. | AtOccurrences of Locus.occurrences
  2. | Unspecified of Evd.Abstraction.abstraction
val default_occurrence_selection : occurrence_selection
type occurrences_selection = occurrence_match_test * occurrence_selection list
val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> int -> occurrences_selection
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
val evar_unify : Evarsolve.unifier
val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> Reductionops.state -> Reductionops.state -> Evarsolve.unification_result
val occur_rigidly : Evarsolve.unify_flags -> 'a -> Evd.evar_map -> (Evar.t * 'b) -> EConstr.t -> bool