package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 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 = {
  1. obj_dir : Names.DirPath.t;
  2. obj_mp : Names.ModPath.t;
  3. 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 =
  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_r =
  1. | Qualid of qualid
  2. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct