package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pr_dirpath : Names.DirPath.t -> Pp.std_ppcmds
val dirpath_of_string : string -> Names.DirPath.t
val string_of_dirpath : Names.DirPath.t -> 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 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.std_ppcmds
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.std_ppcmds
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.kernel_name
val eq_op : object_prefix -> object_prefix -> bool
val make_oname : object_prefix -> Names.Id.t -> object_name
type global_dir_reference =
  1. | DirOpenModule of object_prefix
  2. | DirOpenModtype of object_prefix
  3. | DirOpenSection of object_prefix
  4. | DirModule of object_prefix
  5. | DirClosedSection of Names.DirPath.t
val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool
type reference =
  1. | Qualid of qualid Loc.located
  2. | Ident of Names.Id.t Loc.located
val eq_reference : reference -> reference -> bool
val qualid_of_reference : reference -> qualid Loc.located
val string_of_reference : reference -> string
val pr_reference : reference -> Pp.std_ppcmds
val loc_of_reference : reference -> Loc.t option
val join_reference : reference -> reference -> reference
val make_short_qualid : Names.Id.t -> qualid
val qualid_of_sp : full_path -> qualid
OCaml

Innovation. Community. Security.