Module `Libnames`Source

Sourceval dirpath_of_string : string -> Names.DirPath.t

Dirpaths

Sourceval pop_dirpath : Names.DirPath.t -> Names.DirPath.t

Pop the suffix of a DirPath.t. Raises a Failure for an empty path

Sourceval pop_dirpath_n : int -> Names.DirPath.t -> Names.DirPath.t

Pop the suffix n times

Sourceval split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t

Immediate prefix and basename of a DirPath.t. May raise Failure

Source

val add_dirpath_suffix : 
  Names.DirPath.t ->
  Names.module_ident ->
  Names.DirPath.t

Source

val add_dirpath_prefix : 
  Names.module_ident ->
  Names.DirPath.t ->
  Names.DirPath.t

Sourceval chop_dirpath : int -> Names.DirPath.t -> Names.DirPath.t * Names.DirPath.t

Sourceval append_dirpath : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t

Sourceval drop_dirpath_prefix : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t

Sourceval is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool

Sourceval is_dirpath_suffix_of : Names.DirPath.t -> Names.DirPath.t -> bool

Sourcetype full_path

Full paths are absolute paths of declarations

Sourceval eq_full_path : full_path -> full_path -> bool

Sourceval make_path : Names.DirPath.t -> Names.Id.t -> full_path

Constructors of full_path

Sourceval repr_path : full_path -> Names.DirPath.t * Names.Id.t

Destructors of full_path

Sourceval dirpath : full_path -> Names.DirPath.t

Sourceval basename : full_path -> Names.Id.t

Sourceval path_of_string : string -> full_path

Parsing and printing of section path as "coq_root.module.id"

Sourceval string_of_path : full_path -> string

Sourceval pr_path : full_path -> Pp.t

Sourcemodule Spmap : CSig.MapS with type key = full_path

...

A qualid is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial qualifications of absolute names, including single identifiers. The qualid are used to access the name table.

Sourcetype qualid_r

Sourcetype qualid = qualid_r CAst.t

Sourceval make_qualid : ?loc:Loc.t -> Names.DirPath.t -> Names.Id.t -> qualid

Sourceval repr_qualid : qualid -> Names.DirPath.t * Names.Id.t

Sourceval qualid_eq : qualid -> qualid -> bool

Sourceval is_qualid_suffix_of_full_path : qualid -> full_path -> bool

Sourceval pr_qualid : qualid -> Pp.t

Sourceval string_of_qualid : qualid -> string

Sourceval qualid_of_string : ?loc:Loc.t -> string -> qualid

Turns an absolute name, a dirpath, or an Id.t into a qualified name denoting the same name

Sourceval qualid_of_path : ?loc:Loc.t -> full_path -> qualid

Sourceval qualid_of_dirpath : ?loc:Loc.t -> Names.DirPath.t -> qualid

Sourceval qualid_of_ident : ?loc:Loc.t -> Names.Id.t -> qualid

Sourceval qualid_of_lident : Names.lident -> qualid

Sourceval qualid_is_ident : qualid -> bool

Sourceval qualid_path : qualid -> Names.DirPath.t

Sourceval qualid_basename : qualid -> Names.Id.t

Sourceval idset_mem_qualid : qualid -> Names.Id.Set.t -> bool

false when the qualid is not an ident

...

Sourceval coq_root : Names.module_ident

This is the root of the standard library of Coq

Sourceval coq_string : string

Sourceval default_root_prefix : Names.DirPath.t

This is the default root prefix for developments which doesn't mention a root

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Libnames/index.html

Module `Libnames`Source

...

...

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Libnames/index.html

Module LibnamesSource

...

...

Module `Libnames`Source