Unification (coq-core.Unification)

type core_unify_flags = {

modulo_conv_on_closed_terms : TransparentState.t option;

use_metas_eagerly_in_conv_on_closed_terms : bool;

use_evars_eagerly_in_conv_on_closed_terms : bool;

modulo_delta : TransparentState.t;

modulo_delta_types : TransparentState.t;

check_applied_meta_types : bool;

use_pattern_unification : bool;

use_meta_bound_pattern_unification : bool;

allowed_evars : Evarsolve.AllowedEvars.t;

restrict_conv_on_strict_subterms : bool;

modulo_betaiota : bool;

modulo_eta : bool;

}

type unify_flags = {

core_unify_flags : core_unify_flags;

merge_unify_flags : core_unify_flags;

subterm_unify_flags : core_unify_flags;

allow_K_in_toplevel_higher_order_unification : bool;

resolve_evars : bool;

}

val default_core_unify_flags : unit -> core_unify_flags

val default_no_delta_core_unify_flags : unit -> core_unify_flags

val default_unify_flags : unit -> unify_flags

val default_no_delta_unify_flags : TransparentState.t -> unify_flags

val elim_flags : unit -> unify_flags

val elim_no_delta_flags : unit -> unify_flags

val is_keyed_unification : unit -> bool

val w_unify : 
  Environ.env ->
  Evd.evar_map ->
  Evd.conv_pb ->
  ?flags:unify_flags ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map

The "unique" unification function

val w_unify_to_subterm : 
  Environ.env ->
  Evd.evar_map ->
  ?flags:unify_flags ->
  (EConstr.constr * EConstr.constr) ->
  Evd.evar_map * EConstr.constr

w_unify_to_subterm env m (c,t) performs unification of c with a subterm of t. Constraints are added to m and the matched subterm of t is also returned.

val w_unify_to_subterm_all : 
  Environ.env ->
  Evd.evar_map ->
  ?flags:unify_flags ->
  (EConstr.constr * EConstr.constr) ->
  Evd.evar_map list

val w_unify_meta_types : 
  Environ.env ->
  ?flags:unify_flags ->
  Evd.evar_map ->
  Evd.evar_map

val w_coerce_to_type : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.types ->
  EConstr.types ->
  Evd.evar_map * EConstr.constr

w_coerce_to_type env evd c ctyp typ tries to coerce c of type ctyp so that its gets type typ; typ may contain metavariables

exception PatternNotFound

type prefix_of_inductive_support_flag = bool

type abstraction_request =

| AbstractPattern of prefix_of_inductive_support_flag
  * EConstr.types ->
  bool
  * Names.Name.t
  * Evd.evar_map option * EConstr.constr
  * Locus.clause
  * bool

| AbstractExact of Names.Name.t
  * EConstr.constr
  * EConstr.types option
  * Locus.clause
  * bool

type 'r abstraction_result =
  Names.Id.t
  * Environ.named_context_val
  * EConstr.named_declaration list
  * Names.Id.t option
  * EConstr.types
  * (Evd.evar_map * EConstr.constr) option

val make_abstraction : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  abstraction_request ->
  'r abstraction_result

val pose_all_metas_as_evars : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val abstract_list_all : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  EConstr.constr list ->
  Evd.evar_map * (EConstr.constr * EConstr.types)

abstract_list_all env evd t c l abstracts the terms in l over c to get a term of type t (exported for inv.ml)

type metabinding =
  Constr.metavariable
  * EConstr.constr
  * (Evd.instance_constraint * Evd.instance_typing_status)

type subst0 =
  Evd.evar_map
  * metabinding list
  * ((Environ.env * int) * EConstr.existential * EConstr.t) list

val w_merge : Environ.env -> bool -> core_unify_flags -> subst0 -> Evd.evar_map

val unify_0 : 
  Environ.env ->
  Evd.evar_map ->
  Evd.conv_pb ->
  core_unify_flags ->
  EConstr.types ->
  EConstr.types ->
  subst0