package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module type Nametab.NAMETABSource

Common APIs on name tables.

Sourcetype elt

The type of the elements of the name table (eg ModPath.t)

Sourceval push : visibility -> Libnames.full_path -> elt -> unit

Add an element or modify its visibility. With visibility Until, assume the element is new. With visibility Exactly, assume the element is not new.

Sourceval remove : Libnames.full_path -> elt -> unit

Remove an element.

Sourceval shortest_qualid_gen : ?loc:Loc.t -> (Names.Id.t -> bool) -> elt -> Libnames.qualid

shortest_qualid_gen avoid v: given an object v with full name Mylib.A.B.x, try to find the shortest among x, B.x, A.B.x and Mylib.A.B.x that denotes the same object. If avoid is true on x it is assumed to denote something else (so B.x is the shortest qualid that could be returned).

Sourceval shortest_qualid : ?loc:Loc.t -> Names.Id.Set.t -> elt -> Libnames.qualid

Like shortest_qualid_gen but using an id set instead of a closure.

Sourceval pr : elt -> Pp.t

Print using shortest_qualid and empty avoid set.

Sourceval locate : Libnames.qualid -> elt

Globalize the given user-level reference. If any warnings are associated with the produced object, print them unless nowarn:true was given.

Sourceval locate_all : Libnames.qualid -> elt list

Locate all elements with a given suffix. If the qualid is a valid absolute name, that element is first in the list.

Sourceval completion_candidates : Libnames.qualid -> elt list

Return the elements that have the qualid as a prefix. UIs will usually compose with shortest_qualid. Experimental APIs, please tell us if you use it.

Sourceval to_path : elt -> Libnames.full_path

Return the absolute name for the given element.

Sourceval of_path : Libnames.full_path -> elt

Return an element bound to an absolute path.

Sourceval exists : Libnames.full_path -> bool

Returns whether this absolute path is taken.