coq 8.8.1 · OCaml Package

val dirpath_of_string : string -> Names.DirPath.t

val pr_dirpath : Names.DirPath.t -> Pp.t

deprecated Alias for DirPath.print

val string_of_dirpath : Names.DirPath.t -> string

deprecated Alias for DirPath.to_string

val pop_dirpath : Names.DirPath.t -> Names.DirPath.t

val pop_dirpath_n : int -> Names.DirPath.t -> Names.DirPath.t

val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t

val add_dirpath_suffix : 
  Names.DirPath.t ->
  Names.module_ident ->
  Names.DirPath.t

val add_dirpath_prefix : 
  Names.module_ident ->
  Names.DirPath.t ->
  Names.DirPath.t

val chop_dirpath : int -> Names.DirPath.t -> Names.DirPath.t * Names.DirPath.t

val append_dirpath : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t

val drop_dirpath_prefix : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t

val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool

val is_dirpath_suffix_of : Names.DirPath.t -> Names.DirPath.t -> bool

module Dirset : sig ... end

module Dirmap : sig ... end

type full_path

val eq_full_path : full_path -> full_path -> bool

val make_path : Names.DirPath.t -> Names.Id.t -> full_path

val repr_path : full_path -> Names.DirPath.t * Names.Id.t

val dirpath : full_path -> Names.DirPath.t

val basename : full_path -> Names.Id.t

val path_of_string : string -> full_path

val string_of_path : full_path -> string

val pr_path : full_path -> Pp.t

module Spmap : sig ... end

val restrict_path : int -> full_path -> full_path

type qualid

val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid

val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t

val qualid_eq : qualid -> qualid -> bool

val pr_qualid : qualid -> Pp.t

val string_of_qualid : qualid -> string

val qualid_of_string : string -> qualid

val qualid_of_path : full_path -> qualid

val qualid_of_dirpath : Names.DirPath.t -> qualid

val qualid_of_ident : Names.Id.t -> qualid

type object_name = full_path * Names.KerName.t

type object_prefix = {

obj_dir : Names.DirPath.t;
obj_mp : Names.ModPath.t;
obj_sec : Names.DirPath.t;

}

val eq_op : object_prefix -> object_prefix -> bool

val make_oname : object_prefix -> Names.Id.t -> object_name

type global_dir_reference =

| DirOpenModule of object_prefix
| DirOpenModtype of object_prefix
| DirOpenSection of object_prefix
| DirModule of object_prefix
| DirClosedSection of Names.DirPath.t

val eq_global_dir_reference : 
  global_dir_reference ->
  global_dir_reference ->
  bool

type reference_r =

| Qualid of qualid
| Ident of Names.Id.t

type reference = reference_r CAst.t

val eq_reference : reference -> reference -> bool

val qualid_of_reference : reference -> qualid CAst.t

val string_of_reference : reference -> string

val pr_reference : reference -> Pp.t

val join_reference : reference -> reference -> reference

val default_library : Names.DirPath.t

val coq_root : Names.module_ident

val coq_string : string

val default_root_prefix : Names.DirPath.t

val make_short_qualid : Names.Id.t -> qualid

deprecated Alias for qualid_of_ident

val qualid_of_sp : full_path -> qualid

deprecated Alias for qualid_of_sp

package coq