package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val make_ident : string -> int option -> Names.Id.t
val repr_ident : Names.Id.t -> string * int option
val atompart_of_id : Names.Id.t -> string
val root_of_id : Names.Id.t -> Names.Id.t
val add_suffix : Names.Id.t -> string -> Names.Id.t
val add_prefix : string -> Names.Id.t -> Names.Id.t
val has_subscript : Names.Id.t -> bool
val increment_subscript : Names.Id.t -> Names.Id.t
val forget_subscript : Names.Id.t -> Names.Id.t
module Name : sig ... end
val pr_meta : Constr.metavariable -> Pp.t
val string_of_meta : Constr.metavariable -> string
val out_name : Name.t -> Names.Id.t
  • deprecated Same as [Name.get_id]
val name_fold : (Names.Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
  • deprecated Same as [Name.fold_right]
val name_iter : (Names.Id.t -> unit) -> Name.t -> unit
  • deprecated Same as [Name.iter]
val name_app : (Names.Id.t -> Names.Id.t) -> Name.t -> Name.t
  • deprecated Same as [Name.map]
val name_fold_map : ('a -> Names.Id.t -> 'a * Names.Id.t) -> 'a -> Name.t -> 'a * Name.t
  • deprecated Same as [Name.fold_left_map]
val name_max : Name.t -> Name.t -> Name.t
  • deprecated Same as [Name.pick]
val name_cons : Name.t -> Names.Id.t list -> Names.Id.t list
  • deprecated Same as [Name.cons]
val pr_name : Name.t -> Pp.t
  • deprecated Same as [Name.print]
val pr_id : Names.Id.t -> Pp.t
  • deprecated Same as [Names.Id.print]
val pr_lab : Names.Label.t -> Pp.t
  • deprecated Same as [Names.Label.print]
val default_library : Names.DirPath.t
  • deprecated Same as [Libnames.default_library]
val coq_root : Names.module_ident
  • deprecated Same as [Libnames.coq_root]
val coq_string : string
  • deprecated Same as [Libnames.coq_string]
val default_root_prefix : Names.DirPath.t
  • deprecated Same as [Libnames.default_root_prefix]
OCaml

Innovation. Community. Security.