Module `Unification`Source

Sourcetype 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;

}

Sourcetype 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;

}

Sourceval default_core_unify_flags : unit -> core_unify_flags

Sourceval default_no_delta_core_unify_flags : unit -> core_unify_flags

Sourceval default_unify_flags : unit -> unify_flags

Sourceval default_no_delta_unify_flags : TransparentState.t -> unify_flags

Sourceval elim_flags : unit -> unify_flags

Sourceval elim_no_delta_flags : unit -> unify_flags

Sourceval is_keyed_unification : unit -> bool

Source

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

Source

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.

Source

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

Source

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

Source

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

Sourceexception PatternNotFound

Sourcetype prefix_of_inductive_support_flag = bool

Sourcetype abstraction_request =

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

Source

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

Source

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

Source

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

Source

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)

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Unification/index.html

Module `Unification`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Unification/index.html

Module UnificationSource

Module `Unification`Source