package coq

  1. Overview
  2. Docs
On This Page
  1. ...
  2. ...
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val dirpath_of_string : string -> Names.DirPath.t

Dirpaths

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

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

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

Pop the suffix n times

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

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

val add_dirpath_suffix : Names.DirPath.t -> Names.module_ident -> Names.DirPath.t
val add_dirpath_prefix : Names.module_ident -> Names.DirPath.t -> Names.DirPath.t
val chop_dirpath : int -> Names.DirPath.t -> Names.DirPath.t * Names.DirPath.t
val drop_dirpath_prefix : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t
val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
val is_dirpath_suffix_of : Names.DirPath.t -> Names.DirPath.t -> bool
type full_path

Full paths are absolute paths of declarations

val eq_full_path : full_path -> full_path -> bool
val make_path : Names.DirPath.t -> Names.Id.t -> full_path

Constructors of full_path

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

Destructors of full_path

val dirpath : full_path -> Names.DirPath.t
val basename : full_path -> Names.Id.t
val path_of_string : string -> full_path

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

val string_of_path : full_path -> string
val pr_path : full_path -> Pp.t
module 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.

type qualid_r
type qualid = qualid_r CAst.t
val make_qualid : ?loc:Loc.t -> Names.DirPath.t -> Names.Id.t -> qualid
val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
val qualid_eq : qualid -> qualid -> bool
val pr_qualid : qualid -> Pp.t
val string_of_qualid : qualid -> string
val 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

val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
val qualid_of_dirpath : ?loc:Loc.t -> Names.DirPath.t -> qualid
val qualid_of_ident : ?loc:Loc.t -> Names.Id.t -> qualid
val qualid_of_lident : Names.lident -> qualid
val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> Names.DirPath.t
val qualid_basename : qualid -> Names.Id.t
val idset_mem_qualid : qualid -> Names.Id.Set.t -> bool

false when the qualid is not an ident

...
val default_library : Names.DirPath.t

some preset paths

val coq_root : Names.module_ident

This is the root of the standard library of Coq

val coq_string : string
val default_root_prefix : Names.DirPath.t

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

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