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 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_r
type qualid = qualid_r CAst.t
val make_qualid : ?loc:Loc.t -> 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 : ?loc:Loc.t -> string -> qualid
val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
val qualid_of_dirpath : ?loc:Loc.t -> Names.DirPath.t -> qualid
val qualid_of_ident : ?loc:Loc.t -> Names.Id.t -> qualid
val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> Names.DirPath.t
val qualid_basename : qualid -> Names.Id.t
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
val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool
val default_library : Names.DirPath.t
val coq_root : Names.module_ident
val coq_string : string
val default_root_prefix : Names.DirPath.t
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