coq 8.8.1 · OCaml Package

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 option) ->
  delta_resolver ->
  delta_resolver

val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

val mp_of_delta : delta_resolver -> Names.ModPath.t -> Names.ModPath.t

val kn_of_delta : delta_resolver -> Names.KerName.t -> Names.KerName.t

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 mind_of_deltas_kn : 
  delta_resolver ->
  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 add_mbid : 
  Names.MBId.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution ->
  substitution

val add_mp : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution ->
  substitution

val map_mbid : 
  Names.MBId.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution

val map_mp : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution

val join : substitution -> substitution -> substitution

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 subst_mp : substitution -> Names.ModPath.t -> Names.ModPath.t

val subst_mind : substitution -> Names.MutInd.t -> Names.MutInd.t

val subst_ind : substitution -> Names.inductive -> Names.inductive

val subst_pind : substitution -> Constr.pinductive -> Constr.pinductive

val subst_kn : substitution -> Names.KerName.t -> Names.KerName.t

val subst_con : 
  substitution ->
  Constr.pconstant ->
  Names.Constant.t * Constr.constr

val subst_pcon : substitution -> Constr.pconstant -> Constr.pconstant

val subst_pcon_term : 
  substitution ->
  Constr.pconstant ->
  Constr.pconstant * Constr.constr

val subst_con_kn : 
  substitution ->
  Names.Constant.t ->
  Names.Constant.t * Constr.constr

val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t

val subst_evaluable_reference : 
  substitution ->
  Names.evaluable_global_reference ->
  Names.evaluable_global_reference

val replace_mp_in_kn : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  Names.KerName.t ->
  Names.KerName.t

val subst_mps : substitution -> Constr.constr -> Constr.constr

val occur_mbid : Names.MBId.t -> substitution -> bool

val repr_substituted : 'a substituted -> substitution list option * 'a

val force_constr : Constr.constr substituted -> Constr.constr

val subst_constr : 
  substitution ->
  Constr.constr substituted ->
  Constr.constr substituted

package coq