(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* unit val check_ident_soft : string -> unit (** Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier val id_ord : identifier -> identifier -> int val id_eq : identifier -> identifier -> bool (** Identifiers sets and maps *) module Idset : Set.S with type elt = identifier module Idpred : Predicate.S with type elt = identifier module Idmap : sig include Map.S with type key = identifier val exists : (identifier -> 'a -> bool) -> 'a t -> bool val singleton : key -> 'a -> 'a t end (** {6 Various types based on identifiers } *) type name = Name of identifier | Anonymous type variable = identifier val name_eq : name -> name -> bool (** {6 Directory paths = section names paths } *) type module_ident = identifier module ModIdmap : Map.S with type key = module_ident type dir_path val dir_path_ord : dir_path -> dir_path -> int val dir_path_eq : dir_path -> dir_path -> bool (** Inner modules idents on top of list (to improve sharing). For instance: A.B.C is ["C";"B";"A"] *) val make_dirpath : module_ident list -> dir_path val repr_dirpath : dir_path -> module_ident list val empty_dirpath : dir_path val is_empty_dirpath : dir_path -> bool (** Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string (** {6 Names of structure elements } *) type label val mk_label : string -> label val string_of_label : label -> string val pr_label : label -> Pp.std_ppcmds val label_of_id : identifier -> label val id_of_label : label -> identifier val eq_label : label -> label -> bool module Labset : Set.S with type elt = label module Labmap : Map.S with type key = label (** {6 Unique names for bound modules } *) type mod_bound_id val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool (** The first argument is a file name - to prevent conflict between different files *) val make_mbid : dir_path -> identifier -> mod_bound_id val repr_mbid : mod_bound_id -> int * identifier * dir_path val id_of_mbid : mod_bound_id -> identifier val debug_string_of_mbid : mod_bound_id -> string val string_of_mbid : mod_bound_id -> string (** {6 The module part of the kernel name } *) type module_path = | MPfile of dir_path | MPbound of mod_bound_id | MPdot of module_path * label val mp_ord : module_path -> module_path -> int val mp_eq : module_path -> module_path -> bool val check_bound_mp : module_path -> bool val string_of_mp : module_path -> string module MPset : Set.S with type elt = module_path module MPmap : Map.S with type key = module_path (** Initial "seed" of the unique identifier generator *) val initial_dir : dir_path (** Name of the toplevel structure *) val initial_path : module_path (** [= MPfile initial_dir] *) (** {6 The absolute names of objects seen by kernel } *) type kernel_name (** Constructor and destructor *) val make_kn : module_path -> dir_path -> label -> kernel_name val repr_kn : kernel_name -> module_path * dir_path * label val modpath : kernel_name -> module_path val label : kernel_name -> label val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds val kn_ord : kernel_name -> kernel_name -> int module KNset : Set.S with type elt = kernel_name module KNpred : Predicate.S with type elt = kernel_name module KNmap : Map.S with type key = kernel_name (** {6 Specific paths for declarations } *) type constant type mutual_inductive (** Beware: first inductive has index 0 *) type inductive = mutual_inductive * int (** Beware: first constructor has index 1 *) type constructor = inductive * int (** *_env modules consider an order on user part of names the others consider an order on canonical part of names*) module Cmap : Map.S with type key = constant module Cmap_env : Map.S with type key = constant module Cpred : Predicate.S with type elt = constant module Cset : Set.S with type elt = constant module Cset_env : Set.S with type elt = constant module Mindmap : Map.S with type key = mutual_inductive module Mindmap_env : Map.S with type key = mutual_inductive module Mindset : Set.S with type elt = mutual_inductive module Indmap : Map.S with type key = inductive module Constrmap : Map.S with type key = constructor module Indmap_env : Map.S with type key = inductive module Constrmap_env : Map.S with type key = constructor val constant_of_kn : kernel_name -> constant val constant_of_kn_equiv : kernel_name -> kernel_name -> constant val make_con : module_path -> dir_path -> label -> constant val make_con_equiv : module_path -> module_path -> dir_path -> label -> constant val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * dir_path * label val eq_constant : constant -> constant -> bool val con_with_label : constant -> label -> constant val string_of_con : constant -> string val con_label : constant -> label val con_modpath : constant -> module_path val pr_con : constant -> Pp.std_ppcmds val debug_pr_con : constant -> Pp.std_ppcmds val debug_string_of_con : constant -> string val mind_of_kn : kernel_name -> mutual_inductive val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive val make_mind : module_path -> dir_path -> label -> mutual_inductive val make_mind_equiv : module_path -> module_path -> dir_path -> label -> mutual_inductive val user_mind : mutual_inductive -> kernel_name val canonical_mind : mutual_inductive -> kernel_name val repr_mind : mutual_inductive -> module_path * dir_path * label val eq_mind : mutual_inductive -> mutual_inductive -> bool val string_of_mind : mutual_inductive -> string val mind_label : mutual_inductive -> label val mind_modpath : mutual_inductive -> module_path val pr_mind : mutual_inductive -> Pp.std_ppcmds val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds val debug_string_of_mind : mutual_inductive -> string val ind_modpath : inductive -> module_path val constr_modpath : constructor -> module_path val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_constructor : constructor -> constructor -> bool (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of constant val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool (** {6 Hash-consing } *) val hcons_string : string -> string val hcons_ident : identifier -> identifier val hcons_name : name -> name val hcons_dirpath : dir_path -> dir_path val hcons_con : constant -> constant val hcons_mind : mutual_inductive -> mutual_inductive val hcons_ind : inductive -> inductive val hcons_construct : constructor -> constructor (******) type 'a tableKey = | ConstKey of constant | VarKey of identifier | RelKey of 'a type transparent_state = Idpred.t * Cpred.t val empty_transparent_state : transparent_state val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state val cst_full_transparent_state : transparent_state type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) type id_key = inv_rel_key tableKey val eq_id_key : id_key -> id_key -> bool (*equalities on constant and inductive names for the checker*) val eq_con_chk : constant -> constant -> bool val eq_ind_chk : inductive -> inductive -> bool