package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
module GlobDirRef : sig ... end
type global_dir_reference = GlobDirRef.t
  • deprecated Use [GlobDirRef.t]
val eq_global_dir_reference : GlobDirRef.t -> GlobDirRef.t -> bool
  • deprecated Use [GlobDirRef.equal]
exception GlobalizationError of Libnames.qualid
val error_global_not_found : Libnames.qualid -> 'a
type visibility =
  1. | Until of int
  2. | Exactly of int
val map_visibility : (int -> int) -> visibility -> visibility
val push_modtype : visibility -> Libnames.full_path -> Names.ModPath.t -> unit
val push_dir : visibility -> Names.DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> Libnames.full_path -> Globnames.syndef_name -> unit
module UnivIdMap : sig ... end
val push_universe : visibility -> Libnames.full_path -> Univ.Level.UGlobal.t -> unit
val locate_constant : Libnames.qualid -> Names.Constant.t
val locate_syndef : Libnames.qualid -> Globnames.syndef_name
val locate_modtype : Libnames.qualid -> Names.ModPath.t
val locate_dir : Libnames.qualid -> GlobDirRef.t
val locate_module : Libnames.qualid -> Names.ModPath.t
val locate_section : Libnames.qualid -> Names.DirPath.t
val locate_universe : Libnames.qualid -> Univ.Level.UGlobal.t
val global_inductive : Libnames.qualid -> Names.inductive
val locate_all : Libnames.qualid -> Names.GlobRef.t list
val locate_extended_all : Libnames.qualid -> Globnames.extended_global_reference list
val locate_extended_all_dir : Libnames.qualid -> GlobDirRef.t list
val locate_extended_all_modtype : Libnames.qualid -> Names.ModPath.t list
val completion_canditates : Libnames.qualid -> Globnames.extended_global_reference list
val global_of_path : Libnames.full_path -> Names.GlobRef.t
val exists_cci : Libnames.full_path -> bool
val exists_modtype : Libnames.full_path -> bool
val exists_dir : Names.DirPath.t -> bool
val exists_section : Names.DirPath.t -> bool
val exists_module : Names.DirPath.t -> bool
val exists_universe : Libnames.full_path -> bool
val full_name_cci : Libnames.qualid -> Libnames.full_path
val full_name_modtype : Libnames.qualid -> Libnames.full_path
val full_name_module : Libnames.qualid -> Names.DirPath.t
val path_of_global : Names.GlobRef.t -> Libnames.full_path
val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
val path_of_modtype : Names.ModPath.t -> Libnames.full_path
val path_of_universe : Univ.Level.UGlobal.t -> Libnames.full_path
val dirpath_of_global : Names.GlobRef.t -> Names.DirPath.t
val basename_of_global : Names.GlobRef.t -> Names.Id.t
val pr_global_env : Names.Id.Set.t -> Names.GlobRef.t -> Pp.t
val shortest_qualid_of_global : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
val shortest_qualid_of_syndef : ?loc:Loc.t -> Names.Id.Set.t -> Globnames.syndef_name -> Libnames.qualid
val shortest_qualid_of_modtype : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_module : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> Libnames.qualid
val absolute_reference : Libnames.full_path -> Names.GlobRef.t
module type UserName = sig ... end
module type EqualityType = sig ... end
module type NAMETREE = sig ... end
module Make (U : UserName) (E : EqualityType) : sig ... end
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