package rocq-runtime

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

Module Nametab.XRefsSource

NAMETAB extended with warnings associated to some of the elements.

include NAMETAB with type elt = Globnames.extended_global_reference

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

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_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.

When visibility is Until, wdata may be Some _ in which case the warning data is associated to the element.

Return the warning data associated to the element.

Emit the given warning data for the given element (if the warning is not disabled).

Sourceval locate : ?nowarn:bool -> Libnames.qualid -> elt

Unless nowarn:false is given, if the found element is associated to a warning, that warning is emitted.