package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.pretyping/Unification/index.html

Module UnificationSource

Meta machinery

These functions are almost deprecated. They were used before the introduction of the full-fledged evar calculus. In an ideal world, they should be removed. Alas, some parts of the code still use them. Do not use in newly-written code.

module Metamap : Util.Map.ExtS with type key = Constr.metavariable and module Set := Metaset
Sourcetype 'a freelisted = private {
  1. rebus : 'a;
  2. freemetas : Metaset.t;
}
Sourceval metavars_of : Evd.econstr -> Metaset.t
Sourcemodule Meta : sig ... end

Metas

Legacy unification
Sourcetype 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;
}
Sourcetype 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;
}
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

The "unique" unification function

Sourceval w_unify_to_subterm : ?metas:Meta.t -> Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Meta.t * 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.

Sourceval w_unify_to_subterm_all : ?metas:Meta.t -> Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Meta.t * Evd.evar_map) list
Sourceval w_unify_meta_types : ?metas:Meta.t -> Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Meta.t * 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

Sourceexception PatternNotFound
Sourcetype prefix_of_inductive_support_flag = bool
Sourcetype abstraction_request =
  1. | AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map option * EConstr.constr * Locus.clause
  2. | AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool
Sourceval pose_all_metas_as_evars : metas:Meta.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * Meta.t * 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)