package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type core_unify_flags = {
  1. modulo_conv_on_closed_terms : TransparentState.t option;
  2. use_metas_eagerly_in_conv_on_closed_terms : bool;
  3. use_evars_eagerly_in_conv_on_closed_terms : bool;
  4. modulo_delta : TransparentState.t;
  5. modulo_delta_types : TransparentState.t;
  6. check_applied_meta_types : bool;
  7. use_pattern_unification : bool;
  8. use_meta_bound_pattern_unification : bool;
  9. allowed_evars : Evarsolve.AllowedEvars.t;
  10. restrict_conv_on_strict_subterms : bool;
  11. modulo_betaiota : bool;
  12. modulo_eta : bool;
}
type unify_flags = {
  1. core_unify_flags : core_unify_flags;
  2. merge_unify_flags : core_unify_flags;
  3. subterm_unify_flags : core_unify_flags;
  4. allow_K_in_toplevel_higher_order_unification : bool;
  5. 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

The "unique" unification function

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

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 =
  1. | AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map option * EConstr.constr * Locus.clause * bool
  2. | AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool
val pose_all_metas_as_evars : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

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 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct