package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception GlobalizationError of Libnames.qualid
val error_global_not_found : Libnames.qualid CAst.t -> 'a
type visibility =
  1. | Until of int
  2. | Exactly of int
val push_modtype : visibility -> Libnames.full_path -> Names.ModPath.t -> unit
val push_syndef : visibility -> Libnames.full_path -> Globnames.syndef_name -> unit
type universe_id = Names.DirPath.t * int
module UnivIdMap : sig ... end
val push_universe : visibility -> Libnames.full_path -> universe_id -> 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_module : Libnames.qualid -> Names.ModPath.t
val locate_section : Libnames.qualid -> Names.DirPath.t
val locate_universe : Libnames.qualid -> universe_id
val global_inductive : Libnames.reference -> Names.inductive
val locate_extended_all : Libnames.qualid -> Globnames.extended_global_reference list
val locate_extended_all_dir : Libnames.qualid -> Libnames.global_dir_reference list
val locate_extended_all_modtype : Libnames.qualid -> Names.ModPath.t list
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 dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
val path_of_modtype : Names.ModPath.t -> Libnames.full_path
val path_of_universe : universe_id -> Libnames.full_path
val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t
val basename_of_global : Globnames.global_reference -> Names.Id.t
val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid
val shortest_qualid_of_syndef : Names.Id.Set.t -> Globnames.syndef_name -> Libnames.qualid
val shortest_qualid_of_modtype : Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_universe : universe_id -> Libnames.qualid
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