package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type allowed_evars =
  1. | AllowAll
  2. | AllowFun of Evar.t -> bool
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 : allowed_evars;
  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
val w_unify_to_subterm_all : Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Evd.evar_map * EConstr.constr) list
val w_unify_meta_types : Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Evd.evar_map
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 * 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
val w_merge : Environ.env -> bool -> core_unify_flags -> subst0 -> Evd.evar_map
val unify_0_with_initial_metas : subst0 -> bool -> Environ.env -> Evd.conv_pb -> core_unify_flags -> EConstr.types -> EConstr.types -> subst0
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