coq 8.7.2 · OCaml Package

type delta_resolver

val empty_delta_resolver : delta_resolver

val add_mp_delta_resolver : 
  Names.module_path ->
  Names.module_path ->
  delta_resolver ->
  delta_resolver

val add_kn_delta_resolver : 
  Names.kernel_name ->
  Names.kernel_name ->
  delta_resolver ->
  delta_resolver

val add_inline_delta_resolver : 
  Names.kernel_name ->
  (int * Term.constr option) ->
  delta_resolver ->
  delta_resolver

val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

val mp_of_delta : delta_resolver -> Names.module_path -> Names.module_path

val kn_of_delta : delta_resolver -> Names.kernel_name -> Names.kernel_name

val constant_of_delta_kn : 
  delta_resolver ->
  Names.kernel_name ->
  Names.constant

val constant_of_deltas_kn : 
  delta_resolver ->
  delta_resolver ->
  Names.kernel_name ->
  Names.constant

val mind_of_delta_kn : 
  delta_resolver ->
  Names.kernel_name ->
  Names.mutual_inductive

val mind_of_deltas_kn : 
  delta_resolver ->
  delta_resolver ->
  Names.kernel_name ->
  Names.mutual_inductive

val inline_of_delta : 
  int option ->
  delta_resolver ->
  (int * Names.kernel_name) list

val mp_in_delta : Names.module_path -> delta_resolver -> bool

val con_in_delta : Names.constant -> delta_resolver -> bool

val mind_in_delta : Names.mutual_inductive -> delta_resolver -> bool

type substitution

val empty_subst : substitution

val is_empty_subst : substitution -> bool

val add_mbid : 
  Names.MBId.t ->
  Names.module_path ->
  delta_resolver ->
  substitution ->
  substitution

val add_mp : 
  Names.module_path ->
  Names.module_path ->
  delta_resolver ->
  substitution ->
  substitution

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

val map_mp : 
  Names.module_path ->
  Names.module_path ->
  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.std_ppcmds

val debug_string_of_delta : delta_resolver -> string

val debug_pr_delta : delta_resolver -> Pp.std_ppcmds

val subst_mp : substitution -> Names.module_path -> Names.module_path

val subst_mind : 
  substitution ->
  Names.mutual_inductive ->
  Names.mutual_inductive

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

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

val subst_kn : substitution -> Names.kernel_name -> Names.kernel_name

val subst_con : substitution -> Term.pconstant -> Names.constant * Term.constr

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

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

val subst_con_kn : 
  substitution ->
  Names.constant ->
  Names.constant * Term.constr

val subst_constant : substitution -> Names.constant -> Names.constant

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

val replace_mp_in_kn : 
  Names.module_path ->
  Names.module_path ->
  Names.kernel_name ->
  Names.kernel_name

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

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

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

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

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

package coq