package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type delta_resolver
val empty_delta_resolver : delta_resolver
val add_mp_delta_resolver : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> delta_resolver
val add_kn_delta_resolver : Names.KerName.t -> Names.KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t
val constant_of_deltas_kn : delta_resolver -> delta_resolver -> Names.KerName.t -> Names.Constant.t
val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
val inline_of_delta : int option -> delta_resolver -> (int * Names.KerName.t) list
val mp_in_delta : Names.ModPath.t -> delta_resolver -> bool
val con_in_delta : Names.Constant.t -> delta_resolver -> bool
val mind_in_delta : Names.MutInd.t -> delta_resolver -> bool
type substitution
val empty_subst : substitution
val is_empty_subst : substitution -> bool
val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
type 'a substituted
val from_val : 'a -> 'a substituted
val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
val subst_substituted : substitution -> 'a substituted -> 'a substituted
val debug_string_of_subst : substitution -> string
val debug_pr_subst : substitution -> Pp.t
val debug_string_of_delta : delta_resolver -> string
val debug_pr_delta : delta_resolver -> Pp.t
val repr_substituted : 'a substituted -> substitution list option * 'a