package coq

  1. Overview
  2. Docs
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.